let n be Element of NAT ; :: thesis: for p1, p2 being Point of (TOP-REAL n) holds p1 is_extremal_in LSeg (p1,p2)
let p1, p2 be Point of (TOP-REAL n); :: thesis: p1 is_extremal_in LSeg (p1,p2)
thus p1 in LSeg (p1,p2) by RLTOPSP1:68; :: according to SPPOL_1:def 1 :: thesis: for p1, p2 being Point of (TOP-REAL n) st p1 in LSeg (p1,p2) & LSeg (p1,p2) c= LSeg (p1,p2) & not p1 = p1 holds
p1 = p2
let q1, q2 be Point of (TOP-REAL n); :: thesis: ( p1 in LSeg (q1,q2) & LSeg (q1,q2) c= LSeg (p1,p2) & not p1 = q1 implies p1 = q2 )
thus ( p1 in LSeg (q1,q2) & LSeg (q1,q2) c= LSeg (p1,p2) & not p1 = q1 implies p1 = q2 ) by Th24; :: thesis: verum