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 A1: ( L is being_line & L = Line x1,x2 ) ; :: thesis: x1 <> x2
then consider y1, y2 being Element of REAL n such that
A2: ( y1 <> y2 & L = Line y1,y2 ) by EUCLID_4:def 2;
( y1 in L & y2 in L ) by A2, EUCLID_4:10;
then consider a being Real such that
A3: y2 - y1 = a * (x2 - x1) by A1, Th36;
thus x1 <> x2 :: thesis: verum

proof

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

end;