theorem Th18: :: JORDAN5D:18

for g being FinSequence of (TOP-REAL 2)
for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ g } holds
X = (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g))