assume A7: x in proj2 " Y ; :: thesis: ex Q being Subset of (TOP-REAL 2) st
( Q is open & Q c= proj2 " Y & x in Q )
then reconsider p = x as Point of (TOP-REAL 2) ;
set p1 = proj2 . p;
proj2 . p in Y by A7, FUNCT_2:38;
then consider g being Real such that
A8: 0 < g and
A9: ].((proj2 . p) - g),((proj2 . p) + g).[ c= Y by A6, RCOMP_1:19;
reconsider g = g as Real ;
reconsider Q = proj2 " ].((proj2 . p) - g),((proj2 . p) + g).[ as Subset of (TOP-REAL 2) ;
take Q = Q; :: thesis: ( Q is open & Q c= proj2 " Y & x in Q )
Q = { |[q3,p3]| where q3, p3 is Real : ( (proj2 . p) - g < p3 & p3 < (proj2 . p) + g ) } by Th20;
hence Q is open by Th21; :: thesis: ( Q c= proj2 " Y & x in Q )
thus Q c= proj2 " Y by A9, RELAT_1:143; :: thesis: x in Q
A10: proj2 . p < (proj2 . p) + g by A8, XREAL_1:29;
then (proj2 . p) - g < proj2 . p by XREAL_1:19;
then proj2 . p in ].((proj2 . p) - g),((proj2 . p) + g).[ by A10;
hence x in Q by FUNCT_2:38; :: thesis: verum