let X be Subset of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in X holds
(proj1 | X) . p = p `1
let p be Point of (TOP-REAL 2); :: thesis: ( p in X implies (proj1 | X) . p = p `1 )
assume p in X ; :: thesis: (proj1 | X) . p = p `1
hence (proj1 | X) . p = proj1 . p by FUNCT_1:49
.= p `1 by Def5 ;
:: thesis: verum