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

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

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

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:38;
then consider g being Real such that
A3: 0 < g and
A4: ].((proj1 . p) - g),((proj1 . p) + g).[ c= Y by A1, RCOMP_1:19;
reconsider g = g as Real ;
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 Th18;
hence Q is open by Th19; :: thesis: ( Q c= proj1 " Y & x in Q )
thus Q c= proj1 " Y by A4, RELAT_1:143; :: thesis: x in Q
A5: proj1 . p < (proj1 . p) + g by A3, XREAL_1:29;
then (proj1 . p) - g < proj1 . p by XREAL_1:19;
then proj1 . p in ].((proj1 . p) - g),((proj1 . p) + g).[ by A5;
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= 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:25; :: thesis: verum

end;

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