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

( 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