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)
proof
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;
let e be object ; :: 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) ;
e = ((1 - lambda) * x1) + (lambda * x2) by A2;
hence e in Line (x1,x2) ; :: thesis: verum