let P, Q be Subset of (TOP-REAL 2); :: thesis: for p1, p2 being Point of (TOP-REAL 2) st P c= Q & P is closed & P is_an_arc_of p1,p2 holds
( First_Point (P,p1,p2,Q) = p1 & Last_Point (P,p1,p2,Q) = p2 )
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P c= Q & P is closed & P is_an_arc_of p1,p2 implies ( First_Point (P,p1,p2,Q) = p1 & Last_Point (P,p1,p2,Q) = p2 ) )
assume that
A1: P c= Q and
A2: P is closed and
A3: P is_an_arc_of p1,p2 ; :: thesis: ( First_Point (P,p1,p2,Q) = p1 & Last_Point (P,p1,p2,Q) = p2 )
A4: p2 in P by A3, TOPREAL1:1;
( P /\ Q = P & p1 in P ) by A1, A3, TOPREAL1:1, XBOOLE_1:28;
hence ( First_Point (P,p1,p2,Q) = p1 & Last_Point (P,p1,p2,Q) = p2 ) by A1, A2, A3, A4, Th3, Th6; :: thesis: verum