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 ) ; :: thesis: Line x1,x2 = Line p1,p2
thus Line x1,x2 c= Line p1,p2 :: according to XBOOLE_0:def 10 :: thesis: Line p1,p2 c= Line x1,x2

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in Line x1,x2 or e in Line p1,p2 )
assume e in Line x1,x2 ; :: thesis: e in Line p1,p2
then consider lambda being Real such that
A1: e = ((1 - lambda) * x1) + (lambda * x2) ;
( (1 - lambda) * p1 = (1 - lambda) * x1 & lambda * p2 = lambda * x2 ) by EUCLID:69;
then e = ((1 - lambda) * p1) + (lambda * p2) by A1, EUCLID:68;
hence e in Line p1,p2 ; :: thesis: verum

end;

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in Line p1,p2 or e in Line x1,x2 )
assume e in Line p1,p2 ; :: thesis: e in Line x1,x2
then consider lambda being Real such that
A2: e = ((1 - lambda) * p1) + (lambda * p2) ;
( (1 - lambda) * p1 = (1 - lambda) * x1 & lambda * p2 = lambda * x2 ) by EUCLID:69;
then e = ((1 - lambda) * x1) + (lambda * x2) by A2, EUCLID:68;
hence e in Line x1,x2 ; :: thesis: verum