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:69; :: 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