:: deftheorem Def5 defines proj1 PSCOMP_1:def 5 :
for b₁ being RealMap of (TOP-REAL 2) holds
( b₁ = proj1 iff for p being Point of (TOP-REAL 2) holds b₁ . p = p `1 );