now :: thesis: for Y being Subset of REAL st Y is open holds
proj2 " Y is open

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

now :: thesis: for x being set holds
( ( 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 ) )

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 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

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:25; :: thesis: verum

end;

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