let n be Element of NAT ; :: thesis: for w1, w2 being Point of (TOP-REAL n) st ( for r being Real holds
( not w1 = r * w2 & not w2 = r * w1 ) ) holds
not 0.REAL n in LSeg w1,w2
let w1, w2 be Point of (TOP-REAL n); :: thesis: ( ( for r being Real holds
( not w1 = r * w2 & not w2 = r * w1 ) ) implies not 0.REAL n in LSeg w1,w2 )
assume A1: for r being Real holds
( not w1 = r * w2 & not w2 = r * w1 ) ; :: thesis: not 0.REAL n in LSeg w1,w2
assume 0.REAL n in LSeg w1,w2 ; :: thesis: contradiction
then 0.REAL n in { (((1 - s) * w1) + (s * w2)) where s is Real : ( 0 <= s & s <= 1 ) } by TOPREAL1:def 3;
then consider s being Real such that
A2: ( 0.REAL n = ((1 - s) * w1) + (s * w2) & 0 <= s & s <= 1 ) ;
(0.REAL n) - (s * w2) = (1 - s) * w1 by A2, EUCLID:52;
then - (s * w2) = (1 - s) * w1 by Th13;
then A3: (- s) * w2 = (1 - s) * w1 by EUCLID:44;

per cases ( - s <> 0 or - s = 0 ) ;

suppose A4: - s <> 0 ; :: thesis: contradiction

(((- s) " ) * (- s)) * w2 = ((- s) " ) * ((1 - s) * w1) by A3, EUCLID:34;
then (((- s) " ) * (- s)) * w2 = (((- s) " ) * (1 - s)) * w1 by EUCLID:34;
then 1 * w2 = (((- s) " ) * (1 - s)) * w1 by A4, XCMPLX_0:def 7;
then w2 = (((- s) " ) * (1 - s)) * w1 by EUCLID:33;
hence contradiction by A1; :: thesis: verum

end;

suppose - s = 0 ; :: thesis: contradiction

then (- s) * w2 = w1 by A3, EUCLID:33;
hence contradiction by A1; :: thesis: verum

end;

end;