let n be Nat; 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); 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
; ex x2 being Element of REAL n st
( p1 = x1 & p2 = x2 & Line (x1,x2) = Line (p1,p2) )
take
x2
; ( p1 = x1 & p2 = x2 & Line (x1,x2) = Line (p1,p2) )
thus
( p1 = x1 & p2 = x2 )
; Line (x1,x2) = Line (p1,p2)
thus
Line (x1,x2) c= Line (p1,p2)
XBOOLE_0:def 10 Line (p1,p2) c= Line (x1,x2)
let e be object ; TARSKI:def 3 ( not e in Line (p1,p2) or e in Line (x1,x2) )
assume
e in Line (p1,p2)
; 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)
; verum