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

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)

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) ;

e = ((1 - lambda) * x1) + (lambda * x2) by A2;

hence e in Line (x1,x2) ; :: thesis: verum

( 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:22;

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 object ; :: according to TARSKI:def 3 :: thesis: ( not e in Line (p1,p2) or e in Line (x1,x2) )
let e be object ; :: 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) ;

e = ((1 - lambda) * p1) + (lambda * p2) by A1;

hence e in Line (p1,p2) ; :: thesis: verum

end;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) ;

e = ((1 - lambda) * p1) + (lambda * p2) by A1;

hence e in Line (p1,p2) ; :: thesis: verum

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) ;

e = ((1 - lambda) * x1) + (lambda * x2) by A2;

hence e in Line (x1,x2) ; :: thesis: verum