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;

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 ) )end;

hence
( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed )
by A15, A16, TOPS_1:8; :: thesis: verumper 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;

end;

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;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

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;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

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;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

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;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