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 ) )
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:64;
then A1: P /\ (Vertical_Line e) <> {} by XBOOLE_0:def 7;
consider x being Element of P /\ (Vertical_Line e);
A2: ( x in P & x in Vertical_Line e ) by A1, XBOOLE_0:def 4;
then x in { p3 where p3 is Point of (TOP-REAL 2) : p3 `1 = e } by JORDAN6:def 6;
then consider p4 being Point of (TOP-REAL 2) such that
A3: ( p4 = x & p4 `1 = e ) ;
thus ex p3 being Point of (TOP-REAL 2) st
( p3 in P & p3 `1 = e ) by A2, A3; :: thesis: verum