let r be Real; :: thesis: for X being Subset of (TOP-REAL 2) st r in proj2 .: X holds
ex x being Point of (TOP-REAL 2) st
( x in X & proj2 . x = r )
let X be Subset of (TOP-REAL 2); :: thesis: ( r in proj2 .: X implies ex x being Point of (TOP-REAL 2) st
( x in X & proj2 . x = r ) )
assume r in proj2 .: X ; :: thesis: ex x being Point of (TOP-REAL 2) st
( x in X & proj2 . x = r )
then ex x being object st
( x in the carrier of (TOP-REAL 2) & x in X & proj2 . x = r ) by FUNCT_2:64;
hence ex x being Point of (TOP-REAL 2) st
( x in X & proj2 . x = r ) ; :: thesis: verum