Does the SQL standard actually define LATERAL anywhere?

As implemented in HEAD, LATERAL means to run a nestloop in which the
lateral-referencing query is run once per row of the referenced table,
and the resulting rows are joined to just that row of the referenced
table. So for example:

# select * from (values (2),(4)) v(x), lateral generate_series(1,x);
x | generate_series
---+-----------------
2 | 1
2 | 2
4 | 1
4 | 2
4 | 3
4 | 4
(6 rows)

It suddenly struck me though that there's another plausible
interpretation of this syntax: perhaps we should generate all the rows
of the referencing query as above, and then join them to *all* rows of
the rest of the query. That is, should the above query generate

x | generate_series
---+-----------------
2 | 1
2 | 1
2 | 2
2 | 2
2 | 3
2 | 4
4 | 1
4 | 1
4 | 2
4 | 2
4 | 3
4 | 4
(12 rows)

This behavior doesn't seem as useful to me --- I think you'd nearly
always end up adding additional WHERE clauses to get rid of the extra
rows. However, there should not be any judgment calls involved here;
this is a spec-defined syntax so surely the SQL standard ought to tell
us what to do. But I'm darned if I see anything in the standard that
defines the actual *behavior* of a LATERAL query.

Please point out chapter and verse of what I'm missing. Or, perhaps
we can hold some committee members' feet to the fire for a ruling?

regards, tom lane