now

let Y be Subset of REAL ; :: thesis: ( Y is open implies proj2 " Y is open )
assume A7: Y is open ; :: thesis: proj2 " Y is open
set p1Y = proj2 " Y;

now

let x be set ; :: thesis: ( ( x in proj2 " Y implies ex Q being Subset of (TOP-REAL 2) st
( Q is open & Q c= proj2 " Y & x in Q ) ) & ( ex Q being Subset of (TOP-REAL 2) st
( Q is open & Q c= proj2 " Y & x in Q ) implies x in proj2 " Y ) )

hereby :: thesis: ( ex Q being Subset of (TOP-REAL 2) st
( Q is open & Q c= proj2 " Y & x in Q ) implies x in proj2 " Y )

assume A8: 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 A8, FUNCT_2:46;
then consider g being real number such that
A9: 0 < g and
A10: ].((proj2 . p) - g),((proj2 . p) + g).[ c= Y by A7, RCOMP_1:40;
reconsider g = g as Real by XREAL_0:def 1;
A11: proj2 . p < (proj2 . p) + g by A9, XREAL_1:31;
then (proj2 . p) - g < proj2 . p by XREAL_1:21;
then A12: proj2 . p in ].((proj2 . p) - g),((proj2 . p) + g).[ by A11;
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 Th67;
hence Q is open by Th68; :: thesis: ( Q c= proj2 " Y & x in Q )
thus Q c= proj2 " Y by A10, RELAT_1:178; :: thesis: x in Q
thus x in Q by A12, FUNCT_2:46; :: thesis: verum

end;

assume ex Q being Subset of (TOP-REAL 2) st
( Q is open & Q c= proj2 " Y & x in Q ) ; :: thesis: x in proj2 " Y
hence x in proj2 " Y ; :: thesis: verum

end;

hence proj2 " Y is open by TOPS_1:57; :: thesis: verum

end;

hence proj2 is continuous by Th54; :: thesis: verum