let n be Element of NAT ; :: thesis: for x1, x2 being Element of REAL n
for L being Element of line_of_REAL n st L is being_line & L = Line x1,x2 holds
x1 <> x2
let x1, x2 be Element of REAL n; :: thesis: for L being Element of line_of_REAL n st L is being_line & L = Line x1,x2 holds
x1 <> x2
let L be Element of line_of_REAL n; :: thesis: ( L is being_line & L = Line x1,x2 implies x1 <> x2 )
assume that
A1: L is being_line and
A2: L = Line x1,x2 ; :: thesis: x1 <> x2
consider y1, y2 being Element of REAL n such that
A3: y1 <> y2 and
A4: L = Line y1,y2 by A1, EUCLID_4:def 2;
( y1 in L & y2 in L ) by A4, EUCLID_4:10;
then consider a being Real such that
A5: y2 - y1 = a * (x2 - x1) by A2, Th36;
thus x1 <> x2 :: thesis: verum

proof

assume x1 = x2 ; :: thesis: contradiction
then y2 - y1 = a * (0* n) by A5, Th7
.= 0* n by EUCLID_4:2 ;
hence contradiction by A3, Th14; :: thesis: verum

end;