let P1 be Subset of (TOP-REAL 2); :: thesis: for r being real number
for p1, p2 being Point of (TOP-REAL 2) st p1 `1 <= r & r <= p2 `1 & P1 is_an_arc_of p1,p2 holds
( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed )
let r be real number ; :: thesis: for p1, p2 being Point of (TOP-REAL 2) st p1 `1 <= r & r <= p2 `1 & P1 is_an_arc_of p1,p2 holds
( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed )
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p1 `1 <= r & r <= p2 `1 & P1 is_an_arc_of p1,p2 implies ( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed ) )
assume A1: ( p1 `1 <= r & r <= p2 `1 & P1 is_an_arc_of p1,p2 ) ; :: thesis: ( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed )
then reconsider P1' = P1 as non empty Subset of (TOP-REAL 2) by TOPREAL1:4;
consider f being Function of I[01] ,((TOP-REAL 2) | P1') such that
A2: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by A1, TOPREAL1:def 2;
A3: [#] ((TOP-REAL 2) | P1) = P1 by PRE_TOPC:def 10;
then reconsider f1 = f as Function of the carrier of I[01] ,the carrier of (TOP-REAL 2) by FUNCT_2:9;
reconsider f2 = f1 as Function of I[01] ,(TOP-REAL 2) ;
reconsider proj11 = proj1 as Function of the carrier of (TOP-REAL 2),REAL ;
reconsider proj12 = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
reconsider g1 = proj11 * f1 as Function of the carrier of I[01] ,REAL ;
reconsider g = g1 as Function of I[01] ,R^1 by TOPMETR:24;
f is continuous by A2, TOPS_2:def 5;
then A4: f2 is continuous by Th4;
proj12 is continuous by TOPREAL5:16;
then A5: g is continuous by A4;
A6: dom f = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
then A7: 0 in dom f by XXREAL_1:1;
A8: 1 in dom f by A6, XXREAL_1:1;
A9: g . 0 = proj1 . p1 by A2, A7, FUNCT_1:23
.= p1 `1 by PSCOMP_1:def 28 ;
A10: g . 1 = proj1 . p2 by A2, A8, FUNCT_1:23
.= p2 `1 by PSCOMP_1:def 28 ;
reconsider P1' = P1' as non empty Subset of (TOP-REAL 2) ;
A11: P1' is closed by A1, COMPTS_1:16, JORDAN5A:1;
A12: Vertical_Line r is closed by Th7;

now

per cases ( g . 0 = g . 1 or g . 0[01] = r or g . 1[01] = r or ( g . 0[01] < r & r < g . 1[01] ) ) by A1, A9, A10, BORSUK_1:def 17, BORSUK_1:def 18, XXREAL_0:1;

case g . 0 = g . 1 ; :: thesis: P1 meets Vertical_Line r

then A13: g . 0 = r by A1, A9, A10, XXREAL_0:1;
A14: f . 0 in rng f by A7, FUNCT_1:def 5;
then f . 0 in P1 by A3;
then reconsider p = f . 0 as Point of (TOP-REAL 2) ;
p `1 = proj1 . (f . 0 ) by PSCOMP_1:def 28
.= r by A7, A13, FUNCT_1:23 ;
then f . 0 in { q where q is Point of (TOP-REAL 2) : q `1 = r } ;
hence P1 meets Vertical_Line r by A3, A14, XBOOLE_0:3; :: thesis: verum

end;

case A15: g . 0[01] = r ; :: thesis: P1 meets Vertical_Line r

A16: f . 0 in rng f by A7, FUNCT_1:def 5;
then f . 0 in P1' by A3;
then reconsider p = f . 0 as Point of (TOP-REAL 2) ;
p `1 = proj1 . (f . 0 ) by PSCOMP_1:def 28
.= r by A7, A15, BORSUK_1:def 17, FUNCT_1:23 ;
then f . 0 in { q where q is Point of (TOP-REAL 2) : q `1 = r } ;
hence P1 meets Vertical_Line r by A3, A16, XBOOLE_0:3; :: thesis: verum

end;

case A17: g . 1[01] = r ; :: thesis: P1 meets Vertical_Line r

A18: f . 1 in rng f by A8, FUNCT_1:def 5;
then f . 1 in P1 by A3;
then reconsider p = f . 1 as Point of (TOP-REAL 2) ;
p `1 = proj1 . (f . 1) by PSCOMP_1:def 28
.= r by A8, A17, BORSUK_1:def 18, FUNCT_1:23 ;
then f . 1 in { q where q is Point of (TOP-REAL 2) : q `1 = r } ;
hence P1 meets Vertical_Line r by A3, A18, XBOOLE_0:3; :: thesis: verum

end;

case ( g . 0[01] < r & r < g . 1[01] ) ; :: thesis: P1 meets Vertical_Line r

then consider r1 being Real such that
A19: ( 0 < r1 & r1 < 1 & g . r1 = r ) by A5, A9, A10, Lm1;
dom f = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
then A20: r1 in dom f by A19, XXREAL_1:1;
A21: [#] ((TOP-REAL 2) | P1) = P1 by PRE_TOPC:def 10;
A22: f . r1 in rng f by A20, FUNCT_1:def 5;
then f . r1 in P1' by A21;
then reconsider p = f . r1 as Point of (TOP-REAL 2) ;
p `1 = proj1 . (f . r1) by PSCOMP_1:def 28
.= r by A19, A20, FUNCT_1:23 ;
then f . r1 in { q where q is Point of (TOP-REAL 2) : q `1 = r } ;
hence P1 meets Vertical_Line r by A21, A22, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

hence ( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed ) by A11, A12, TOPS_1:35; :: thesis: verum