set ZS = Rat-Module ;
let s, t be Element of Rat-Module; :: thesis: ( s <> t implies not {s,t} is linearly-independent )
assume AS: s <> t ; :: thesis: not {s,t} is linearly-independent
assume P1: {s,t} is linearly-independent ; :: thesis: contradiction
consider m, n being Integer such that
P2: ( n > 0 & s = m / n ) by RAT_1:1;
consider p, q being Integer such that
P3: ( q > 0 & t = p / q ) by RAT_1:1;
reconsider b = n * p as Element of INT.Ring by INT_1:def 2;
reconsider a = q * m as Element of INT.Ring by INT_1:def 2;
P4: p <> 0. INT.Ring by AS, P1, P3, ZMODUL02:62;
b * s = (n * p) * (m / n) by LMTFRat2, P2
.= p * m by P2, XCMPLX_1:90
.= (q * m) * (p / q) by P3, XCMPLX_1:90
.= a * t by LMTFRat2, P3 ;
hence contradiction by AS, P1, P2, P4, ZMODUL02:62; :: thesis: verum