reconsider fX2 = Proj2_1 as Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1 by TOPMETR:17;
for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):]
for V being Subset of R^1 st fX2 . 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 & fX2 .: W c= V )

proof

let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: for V being Subset of R^1 st fX2 . 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 & fX2 .: W c= V )
let V be Subset of R^1; :: thesis: ( fX2 . 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 & fX2 .: W c= V ) )
assume that
A1: fX2 . 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 & fX2 .: W c= V )
A3: p = [(p `1),(p `2)] by Lm5, MCART_1:21;
A4: fX2 . p = (p `2) `1 by Def5;
reconsider V1 = V as open Subset of REAL by A2, BORSUK_5:39, TOPMETR:17;
consider g being Real such that
A5: 0 < g and
A6: ].(((p `2) `1) - g),(((p `2) `1) + g).[ c= V1 by A1, A4, RCOMP_1:19;
reconsider g = g as Element of REAL by XREAL_0:def 1;
set W1 = { |[x,y]| where x, y is Real : ( ((p `2) `1) - g < x & x < ((p `2) `1) + g ) } ;
{ |[x,y]| where x, y is Real : ( ((p `2) `1) - g < x & x < ((p `2) `1) + g ) } c= the carrier of (TOP-REAL 2)

proof

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

end;

then reconsider W1 = { |[x,y]| where x, y is Real : ( ((p `2) `1) - g < x & x < ((p `2) `1) + 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 & fX2 .: [:([#] (TOP-REAL 2)),W1:] c= V )
A7: p `2 = |[((p `2) `1),((p `2) `2)]| by EUCLID:53;
A8: ((p `2) `1) - g < ((p `2) `1) - 0 by A5, XREAL_1:15;
((p `2) `1) + 0 < ((p `2) `1) + g by A5, XREAL_1:6;
then p `2 in W1 by A7, A8;
hence p in [:([#] (TOP-REAL 2)),W1:] by A3, ZFMISC_1:def 2; :: thesis: ( [:([#] (TOP-REAL 2)),W1:] is open & fX2 .: [:([#] (TOP-REAL 2)),W1:] c= V )
W1 is open by PSCOMP_1:19;
hence [:([#] (TOP-REAL 2)),W1:] is open by BORSUK_1:6; :: thesis: fX2 .: [:([#] (TOP-REAL 2)),W1:] c= V
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in fX2 .: [:([#] (TOP-REAL 2)),W1:] or b in V )
assume b in fX2 .: [:([#] (TOP-REAL 2)),W1:] ; :: thesis: b in V
then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A9: a in [:([#] (TOP-REAL 2)),W1:] and
A10: fX2 . a = b by FUNCT_2:65;
A11: a = [(a `1),(a `2)] by Lm5, MCART_1:21;
A12: fX2 . a = (a `2) `1 by Def5;
a `2 in W1 by A9, A11, ZFMISC_1:87;
then consider x1, y1 being Real such that
A13: a `2 = |[x1,y1]| and
A14: ((p `2) `1) - g < x1 and
A15: x1 < ((p `2) `1) + g ;
A16: (a `2) `1 = x1 by A13, EUCLID:52;
A17: (((p `2) `1) - g) + g < x1 + g by A14, XREAL_1:6;
A18: ((p `2) `1) - x1 > ((p `2) `1) - (((p `2) `1) + g) by A15, XREAL_1:15;
A19: ((p `2) `1) - x1 < (x1 + g) - x1 by A17, XREAL_1:9;
((p `2) `1) - x1 > - g by A18;
then |.(((p `2) `1) - x1).| < g by A19, SEQ_2:1;
then |.(- (((p `2) `1) - x1)).| < g by COMPLEX1:52;
then |.(x1 - ((p `2) `1)).| < g ;
then (a `2) `1 in ].(((p `2) `1) - g),(((p `2) `1) + g).[ by A16, RCOMP_1:1;
hence b in V by A6, A10, A12; :: thesis: verum

end;

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