now

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

now

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

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

assume A2: x in proj1 " Y ; :: thesis: ex Q being Subset of (TOP-REAL 2) st
( Q is open & Q c= proj1 " Y & x in Q )
then reconsider p = x as Point of (TOP-REAL 2) ;
set p1 = proj1 . p;
proj1 . p in Y by A2, FUNCT_2:46;
then consider g being real number such that
A3: 0 < g and
A4: ].((proj1 . p) - g),((proj1 . p) + g).[ c= Y by A1, RCOMP_1:40;
reconsider g = g as Real by XREAL_0:def 1;
A5: proj1 . p < (proj1 . p) + g by A3, XREAL_1:31;
then (proj1 . p) - g < proj1 . p by XREAL_1:21;
then A6: proj1 . p in ].((proj1 . p) - g),((proj1 . p) + g).[ by A5;
reconsider Q = proj1 " ].((proj1 . p) - g),((proj1 . p) + g).[ as Subset of (TOP-REAL 2) ;
take Q = Q; :: thesis: ( Q is open & Q c= proj1 " Y & x in Q )
Q = { |[q3,p3]| where q3, p3 is Real : ( (proj1 . p) - g < q3 & q3 < (proj1 . p) + g ) } by Th65;
hence Q is open by Th66; :: thesis: ( Q c= proj1 " Y & x in Q )
thus Q c= proj1 " Y by A4, RELAT_1:178; :: thesis: x in Q
thus x in Q by A6, FUNCT_2:46; :: thesis: verum

end;

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

end;

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

end;

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