let n be Element of NAT ; :: thesis: for q1, q2 being Point of (TOP-REAL n) st q1,q2 are_lindependent2 holds
( q1 <> q2 & q1 <> 0.REAL n & q2 <> 0.REAL n )
let q1, q2 be Point of (TOP-REAL n); :: thesis: ( q1,q2 are_lindependent2 implies ( q1 <> q2 & q1 <> 0.REAL n & q2 <> 0.REAL n ) )
assume A1: q1,q2 are_lindependent2 ; :: thesis: ( q1 <> q2 & q1 <> 0.REAL n & q2 <> 0.REAL n )
assume A2: ( q1 = q2 or q1 = 0.REAL n or q2 = 0.REAL n ) ; :: thesis: contradiction

now

per cases ( q1 = q2 or q1 = 0.REAL n or q2 = 0.REAL n ) by A2;

case A3: q1 = q2 ; :: thesis: contradiction

(1 * q1) + ((- 1) * q2) = q1 + (- q2) by EUCLID:33
.= 0.REAL n by A3, EUCLID:40 ;
hence contradiction by A1, Def10; :: thesis: verum

end;

case q1 = 0.REAL n ; :: thesis: contradiction

then (1 * q1) + (0 * q2) = (0.REAL n) + (0 * q2) by EUCLID:32
.= (0.REAL n) + (0.REAL n) by EUCLID:33
.= 0.REAL n by EUCLID:31 ;
hence contradiction by A1, Def10; :: thesis: verum

end;

case q2 = 0.REAL n ; :: thesis: contradiction

then (0 * q1) + (1 * q2) = (0 * q1) + (0.REAL n) by EUCLID:32
.= (0.REAL n) + (0.REAL n) by EUCLID:33
.= 0.REAL n by EUCLID:31 ;
hence contradiction by A1, Def10; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum