let n be Nat; :: thesis: for p1, p2 being Point of (TOP-REAL n) holds
( p1 in LSeg p1,p2 & p2 in LSeg p1,p2 )
let p1, p2 be Point of (TOP-REAL n); :: thesis: ( p1 in LSeg p1,p2 & p2 in LSeg p1,p2 )
( 1 - 0 = 1 & 1 - 1 = 0 & 1 * p1 = p1 & 0 * p1 = 0.REAL n & 0 * p2 = 0.REAL n & p1 + (0.REAL n) = p1 & (0.REAL n) + p2 = p2 & 1 * p2 = p2 ) by EUCLID:31, EUCLID:33;
hence ( p1 in LSeg p1,p2 & p2 in LSeg p1,p2 ) ; :: thesis: verum