theorem Th22: :: PSCOMP_1:22

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