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