theorem Th23: :: PSCOMP_1:23

for X being Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in X holds
(proj2 | X) . p = p `2