let P1 be Subset of (TOP-REAL 2); :: thesis: for r being Real
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; :: 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 that
A1: p1 `1 <= r and
A2: r <= p2 `1 and
A3: P1 is_an_arc_of p1,p2 ; :: thesis: ( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed )
reconsider P19 = P1 as non empty Subset of (TOP-REAL 2) by A3, TOPREAL1:1;
consider f being Function of I[01],((TOP-REAL 2) | P19) such that
A4: f is being_homeomorphism and
A5: f . 0 = p1 and
A6: f . 1 = p2 by A3, TOPREAL1:def 1;
A7: [#] ((TOP-REAL 2) | P1) = P1 by PRE_TOPC:def 5;
then reconsider f1 = f as Function of the carrier of I[01], the carrier of (TOP-REAL 2) by FUNCT_2:7;
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:17;
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:17;
f is continuous by A4, TOPS_2:def 5;
then A8: f2 is continuous by Th3;
A9: proj12 is continuous by TOPREAL5:10;
A10: dom f = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
then A11: 0 in dom f by XXREAL_1:1;
A12: 1 in dom f by A10, XXREAL_1:1;
A13: g . 0 = proj1 . p1 by A5, A11, FUNCT_1:13
.= p1 `1 by PSCOMP_1:def 5 ;
A14: g . 1 = proj1 . p2 by A6, A12, FUNCT_1:13
.= p2 `1 by PSCOMP_1:def 5 ;
reconsider P19 = P19 as non empty Subset of (TOP-REAL 2) ;
A15: P19 is closed by A3, COMPTS_1:7, JORDAN5A:1;
A16: Vertical_Line r is closed by Th6;

now :: thesis: ( ( g . 0 = g . 1 & P1 meets Vertical_Line r ) or ( g . 0[01] = r & P1 meets Vertical_Line r ) or ( g . 1[01] = r & P1 meets Vertical_Line r ) or ( g . 0[01] < r & r < g . 1[01] & P1 meets Vertical_Line r ) )

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, A2, A13, A14, BORSUK_1:def 14, BORSUK_1:def 15, XXREAL_0:1;

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

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

end;

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

A20: f . 0 in rng f by A11, FUNCT_1:def 3;
then f . 0 in P19 by A7;
then reconsider p = f . 0 as Point of (TOP-REAL 2) ;
p `1 = proj1 . (f . 0) by PSCOMP_1:def 5
.= r by A11, A19, BORSUK_1:def 14, FUNCT_1:13 ;
then f . 0 in { q where q is Point of (TOP-REAL 2) : q `1 = r } ;
hence P1 meets Vertical_Line r by A7, A20, XBOOLE_0:3; :: thesis: verum

end;

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

A22: f . 1 in rng f by A12, FUNCT_1:def 3;
then f . 1 in P1 by A7;
then reconsider p = f . 1 as Point of (TOP-REAL 2) ;
p `1 = proj1 . (f . 1) by PSCOMP_1:def 5
.= r by A12, A21, BORSUK_1:def 15, FUNCT_1:13 ;
then f . 1 in { q where q is Point of (TOP-REAL 2) : q `1 = r } ;
hence P1 meets Vertical_Line r by A7, A22, 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
A23: 0 < r1 and
A24: r1 < 1 and
A25: g . r1 = r by A8, A9, Lm1;
dom f = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
then A26: r1 in dom f by A23, A24, XXREAL_1:1;
A27: [#] ((TOP-REAL 2) | P1) = P1 by PRE_TOPC:def 5;
A28: f . r1 in rng f by A26, FUNCT_1:def 3;
then f . r1 in P19 by A27;
then reconsider p = f . r1 as Point of (TOP-REAL 2) ;
p `1 = proj1 . (f . r1) by PSCOMP_1:def 5
.= r by A25, A26, FUNCT_1:13 ;
then f . r1 in { q where q is Point of (TOP-REAL 2) : q `1 = r } ;
hence P1 meets Vertical_Line r by A27, A28, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

hence ( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed ) by A15, A16, TOPS_1:8; :: thesis: verum