let n be Element of NAT ; :: thesis: for x1, x2 being Element of REAL n st x1 // x2 holds
x1,x2 are_ldependent2
let x1, x2 be Element of REAL n; :: thesis: ( x1 // x2 implies x1,x2 are_ldependent2 )
assume x1 // x2 ; :: thesis: x1,x2 are_ldependent2
then consider r being Real such that
A1: x1 = r * x2 by Def1;
assume A2: x1,x2 are_lindependent2 ; :: thesis: contradiction
0* n = x1 - x1 by Th7
.= (1 * x1) + (- (r * x2)) by A1, EUCLID_4:3
.= (1 * x1) + ((- r) * x2) by Th8 ;
hence contradiction by A2, Def2; :: thesis: verum