reconsider fY2 = Proj2_2 as Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1 by TOPMETR:24;
for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):]
for V being Subset of R^1 st fY2 . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & fY2 .: W c= V )

proof

let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: for V being Subset of R^1 st fY2 . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & fY2 .: W c= V )
let V be Subset of R^1 ; :: thesis: ( fY2 . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & fY2 .: W c= V ) )
assume that
A1: fY2 . p in V and
A2: V is open ; :: thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & fY2 .: W c= V )
A3: p = [(p `1 ),(p `2 )] by Lm7, MCART_1:23;
A4: fY2 . p = (p `2 ) `2 by Def6;
reconsider V1 = V as open Subset of REAL by A2, BORSUK_5:62, TOPMETR:24;
consider g being real number such that
A5: 0 < g and
A6: ].(((p `2 ) `2 ) - g),(((p `2 ) `2 ) + g).[ c= V1 by A1, A4, RCOMP_1:40;
reconsider g = g as Element of REAL by XREAL_0:def 1;
set W1 = { |[x,y]| where x, y is Element of REAL : ( ((p `2 ) `2 ) - g < y & y < ((p `2 ) `2 ) + g ) } ;
{ |[x,y]| where x, y is Element of REAL : ( ((p `2 ) `2 ) - g < y & y < ((p `2 ) `2 ) + g ) } c= the carrier of (TOP-REAL 2)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { |[x,y]| where x, y is Element of REAL : ( ((p `2 ) `2 ) - g < y & y < ((p `2 ) `2 ) + g ) } or a in the carrier of (TOP-REAL 2) )
assume a in { |[x,y]| where x, y is Element of REAL : ( ((p `2 ) `2 ) - g < y & y < ((p `2 ) `2 ) + g ) } ; :: thesis: a in the carrier of (TOP-REAL 2)
then ex x, y being Element of REAL st
( a = |[x,y]| & ((p `2 ) `2 ) - g < y & y < ((p `2 ) `2 ) + g ) ;
hence a in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;

then reconsider W1 = { |[x,y]| where x, y is Element of REAL : ( ((p `2 ) `2 ) - g < y & y < ((p `2 ) `2 ) + g ) } as Subset of (TOP-REAL 2) ;
take [:([#] (TOP-REAL 2)),W1:] ; :: thesis: ( p in [:([#] (TOP-REAL 2)),W1:] & [:([#] (TOP-REAL 2)),W1:] is open & fY2 .: [:([#] (TOP-REAL 2)),W1:] c= V )
A7: p `2 = |[((p `2 ) `1 ),((p `2 ) `2 )]| by EUCLID:57;
( ((p `2 ) `2 ) - g < ((p `2 ) `2 ) - 0 & ((p `2 ) `2 ) + 0 < ((p `2 ) `2 ) + g ) by A5, XREAL_1:8, XREAL_1:17;
then p `2 in W1 by A7;
hence p in [:([#] (TOP-REAL 2)),W1:] by A3, ZFMISC_1:def 2; :: thesis: ( [:([#] (TOP-REAL 2)),W1:] is open & fY2 .: [:([#] (TOP-REAL 2)),W1:] c= V )
W1 is open by PSCOMP_1:68;
hence [:([#] (TOP-REAL 2)),W1:] is open by BORSUK_1:46; :: thesis: fY2 .: [:([#] (TOP-REAL 2)),W1:] c= V
let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in fY2 .: [:([#] (TOP-REAL 2)),W1:] or b in V )
assume b in fY2 .: [:([#] (TOP-REAL 2)),W1:] ; :: thesis: b in V
then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A8: a in [:([#] (TOP-REAL 2)),W1:] and
A9: fY2 . a = b by FUNCT_2:116;
A10: a = [(a `1 ),(a `2 )] by Lm7, MCART_1:23;
A11: fY2 . a = (a `2 ) `2 by Def6;
a `2 in W1 by A8, A10, ZFMISC_1:106;
then consider x1, y1 being Element of REAL such that
A12: a `2 = |[x1,y1]| and
A13: ((p `2 ) `2 ) - g < y1 and
A14: y1 < ((p `2 ) `2 ) + g ;
A15: (a `2 ) `2 = y1 by A12, EUCLID:56;
( (((p `2 ) `2 ) - g) + g < y1 + g & ((p `2 ) `2 ) - y1 > ((p `2 ) `2 ) - (((p `2 ) `2 ) + g) ) by A13, A14, XREAL_1:8, XREAL_1:17;
then ( ((p `2 ) `2 ) - y1 < (y1 + g) - y1 & ((p `2 ) `2 ) - y1 > - g ) by XREAL_1:11;
then abs (((p `2 ) `2 ) - y1) < g by SEQ_2:9;
then abs (- (((p `2 ) `2 ) - y1)) < g by COMPLEX1:138;
then abs (y1 - ((p `2 ) `2 )) < g ;
then (a `2 ) `2 in ].(((p `2 ) `2 ) - g),(((p `2 ) `2 ) + g).[ by A15, RCOMP_1:8;
hence b in V by A6, A9, A11; :: thesis: verum

end;

hence Proj2_2 is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1 by JGRAPH_2:20; :: thesis: verum