let P1 be Subset of (); :: thesis: for r being Real
for p1, p2 being Point of () st p1 `1 <= r & r <= p2 `1 & P1 is_an_arc_of p1,p2 holds
( P1 meets Vertical_Line r & P1 /\ () is closed )

let r be Real; :: thesis: for p1, p2 being Point of () st p1 `1 <= r & r <= p2 `1 & P1 is_an_arc_of p1,p2 holds
( P1 meets Vertical_Line r & P1 /\ () is closed )

let p1, p2 be Point of (); :: thesis: ( p1 `1 <= r & r <= p2 `1 & P1 is_an_arc_of p1,p2 implies ( P1 meets Vertical_Line r & P1 /\ () 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 /\ () is closed )
reconsider P19 = P1 as non empty Subset of () by ;
consider f being Function of I,(() | P19) such that
A4: f is being_homeomorphism and
A5: f . 0 = p1 and
A6: f . 1 = p2 by ;
A7: [#] (() | P1) = P1 by PRE_TOPC:def 5;
then reconsider f1 = f as Function of the carrier of I, the carrier of () by FUNCT_2:7;
reconsider f2 = f1 as Function of I,() ;
reconsider proj11 = proj1 as Function of the carrier of (),REAL ;
reconsider proj12 = proj1 as Function of (),R^1 by TOPMETR:17;
reconsider g1 = proj11 * f1 as Function of the carrier of I,REAL ;
reconsider g = g1 as Function of I,R^1 by TOPMETR:17;
f is continuous by ;
then A8: f2 is continuous by Th3;
A9: proj12 is continuous by TOPREAL5:10;
A10: dom f = [.0,1.] by ;
then A11: 0 in dom f by XXREAL_1:1;
A12: 1 in dom f by ;
A13: g . 0 = proj1 . p1 by
.= p1 `1 by PSCOMP_1:def 5 ;
A14: g . 1 = proj1 . p2 by
.= p2 `1 by PSCOMP_1:def 5 ;
reconsider P19 = P19 as non empty Subset of () ;
A15: P19 is closed by ;
A16: Vertical_Line r is closed by Th6;
now :: thesis: ( ( g . 0 = g . 1 & P1 meets Vertical_Line r ) or ( g . 0 = r & P1 meets Vertical_Line r ) or ( g . 1 = r & P1 meets Vertical_Line r ) or ( g . 0 < r & r < g . 1 & P1 meets Vertical_Line r ) )
per cases ( g . 0 = g . 1 or g . 0 = r or g . 1 = r or ( g . 0 < r & r < g . 1 ) ) by ;
case g . 0 = g . 1 ; :: thesis:
then A17: g . 0 = r by ;
A18: f . 0 in rng f by ;
then f . 0 in P1 by A7;
then reconsider p = f . 0 as Point of () ;
p `1 = proj1 . (f . 0) by PSCOMP_1:def 5
.= r by ;
then f . 0 in { q where q is Point of () : q `1 = r } ;
hence P1 meets Vertical_Line r by ; :: thesis: verum
end;
case A19: g . 0 = r ; :: thesis:
A20: f . 0 in rng f by ;
then f . 0 in P19 by A7;
then reconsider p = f . 0 as Point of () ;
p `1 = proj1 . (f . 0) by PSCOMP_1:def 5
.= r by ;
then f . 0 in { q where q is Point of () : q `1 = r } ;
hence P1 meets Vertical_Line r by ; :: thesis: verum
end;
case A21: g . 1 = r ; :: thesis:
A22: f . 1 in rng f by ;
then f . 1 in P1 by A7;
then reconsider p = f . 1 as Point of () ;
p `1 = proj1 . (f . 1) by PSCOMP_1:def 5
.= r by ;
then f . 1 in { q where q is Point of () : q `1 = r } ;
hence P1 meets Vertical_Line r by ; :: thesis: verum
end;
case ( g . 0 < r & r < g . 1 ) ; :: thesis:
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 ;
then A26: r1 in dom f by ;
A27: [#] (() | P1) = P1 by PRE_TOPC:def 5;
A28: f . r1 in rng f by ;
then f . r1 in P19 by A27;
then reconsider p = f . r1 as Point of () ;
p `1 = proj1 . (f . r1) by PSCOMP_1:def 5
.= r by ;
then f . r1 in { q where q is Point of () : q `1 = r } ;
hence P1 meets Vertical_Line r by ; :: thesis: verum
end;
end;
end;
hence ( P1 meets Vertical_Line r & P1 /\ () is closed ) by ; :: thesis: verum