let n be Nat; :: thesis: for p1, p2 being Point of (TOP-REAL n) ex x1, x2 being Element of REAL n st
( p1 = x1 & p2 = x2 & Line x1,x2 = Line p1,p2 )
let p1, p2 be Point of (TOP-REAL n); :: thesis: ex x1, x2 being Element of REAL n st
( p1 = x1 & p2 = x2 & Line x1,x2 = Line p1,p2 )
reconsider x1 = p1, x2 = p2 as Element of REAL n by EUCLID:25;
take x1 ; :: thesis: ex x2 being Element of REAL n st
( p1 = x1 & p2 = x2 & Line x1,x2 = Line p1,p2 )
take x2 ; :: thesis: ( p1 = x1 & p2 = x2 & Line x1,x2 = Line p1,p2 )
thus ( p1 = x1 & p2 = x2 & Line x1,x2 = Line p1,p2 ) ; :: thesis: verum