let n be 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;
( y1 in L & y2 in L ) by A4, EUCLID_4:9;
then consider a being Real such that
A5: y2 - y1 = a * (x2 - x1) by A2, Th31;
thus x1 <> x2 :: thesis: verum
proof
assume x1 = x2 ; :: thesis: contradiction
then y2 - y1 = a * (0* n) by A5, Th2
.= 0* n by EUCLID_4:2 ;
hence contradiction by A3, Th9; :: thesis: verum
end;