let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, p being Point of (TOP-REAL 2)
for e being Real st P is_an_arc_of p1,p2 & p1 `1 <= e & p2 `1 >= e holds
ex p3 being Point of (TOP-REAL 2) st
( p3 in P & p3 `1 = e )
let p1, p2, p be Point of (TOP-REAL 2); :: thesis: for e being Real st P is_an_arc_of p1,p2 & p1 `1 <= e & p2 `1 >= e holds
ex p3 being Point of (TOP-REAL 2) st
( p3 in P & p3 `1 = e )
let e be Real; :: thesis: ( P is_an_arc_of p1,p2 & p1 `1 <= e & p2 `1 >= e implies ex p3 being Point of (TOP-REAL 2) st
( p3 in P & p3 `1 = e ) )
set x = the Element of P /\ (Vertical_Line e);
assume ( P is_an_arc_of p1,p2 & p1 `1 <= e & p2 `1 >= e ) ; :: thesis: ex p3 being Point of (TOP-REAL 2) st
( p3 in P & p3 `1 = e )
then P meets Vertical_Line e by JORDAN6:49;
then A1: P /\ (Vertical_Line e) <> {} by XBOOLE_0:def 7;
then the Element of P /\ (Vertical_Line e) in Vertical_Line e by XBOOLE_0:def 4;
then the Element of P /\ (Vertical_Line e) in { p3 where p3 is Point of (TOP-REAL 2) : p3 `1 = e } by JORDAN6:def 6;
then A2: ex p4 being Point of (TOP-REAL 2) st
( p4 = the Element of P /\ (Vertical_Line e) & p4 `1 = e ) ;
the Element of P /\ (Vertical_Line e) in P by A1, XBOOLE_0:def 4;
hence ex p3 being Point of (TOP-REAL 2) st
( p3 in P & p3 `1 = e ) by A2; :: thesis: verum