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. (TOP-REAL n) & q2 <> 0. (TOP-REAL n) )
let q1, q2 be Point of (TOP-REAL n); :: thesis: ( q1,q2 are_lindependent2 implies ( q1 <> q2 & q1 <> 0. (TOP-REAL n) & q2 <> 0. (TOP-REAL n) ) )
assume A1: q1,q2 are_lindependent2 ; :: thesis: ( q1 <> q2 & q1 <> 0. (TOP-REAL n) & q2 <> 0. (TOP-REAL n) )
assume A2: ( q1 = q2 or q1 = 0. (TOP-REAL n) or q2 = 0. (TOP-REAL n) ) ; :: thesis: contradiction

now

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

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

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

end;

case q1 = 0. (TOP-REAL n) ; :: thesis: contradiction

then (1 * q1) + (0 * q2) = (0. (TOP-REAL n)) + (0 * q2) by EUCLID:28
.= (0. (TOP-REAL n)) + (0. (TOP-REAL n)) by EUCLID:29
.= 0. (TOP-REAL n) by EUCLID:27 ;
hence contradiction by A1, Def10; :: thesis: verum

end;

case q2 = 0. (TOP-REAL n) ; :: thesis: contradiction

then (0 * q1) + (1 * q2) = (0 * q1) + (0. (TOP-REAL n)) by EUCLID:28
.= (0. (TOP-REAL n)) + (0. (TOP-REAL n)) by EUCLID:29
.= 0. (TOP-REAL n) by EUCLID:27 ;
hence contradiction by A1, Def10; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum