set ZS = Rat-Module ;
assume Rat-Module is free ; :: thesis: contradiction
then consider A being Subset of Rat-Module such that
p1: A is base ;

per cases ( for s, t being Element of Rat-Module holds
( not s in A or not t in A or not s <> t ) or ex s, t being Element of Rat-Module st
( s in A & t in A & s <> t ) ) ;

suppose P2: for s, t being Element of Rat-Module holds
( not s in A or not t in A or not s <> t ) ; :: thesis: contradiction

A <> {}

proof

assume A = {} ; :: thesis: contradiction
then A = {} the carrier of Rat-Module ;
then Lin A = (0). Rat-Module by ZMODUL02:67;
hence contradiction by p1; :: thesis: verum

end;

then consider s being object such that
P21: s in A by XBOOLE_0:def 1;
reconsider s = s as Element of Rat-Module by P21;
P23: {s} c= A by ZFMISC_1:31, P21;

now :: thesis: for z being object st z in A holds
z in {s}

let z be object ; :: thesis: ( z in A implies z in {s} )
assume P22: z in A ; :: thesis: z in {s}
then reconsider z0 = z as Element of Rat-Module ;
z0 = s by P21, P22, P2;
hence z in {s} by TARSKI:def 1; :: thesis: verum

end;

then A c= {s} ;
then A = {s} by P23, XBOOLE_0:def 10;
hence contradiction by p1, LMThFRat31; :: thesis: verum

end;

suppose ex s, t being Element of Rat-Module st
( s in A & t in A & s <> t ) ; :: thesis: contradiction

then consider s, t being Element of Rat-Module such that
P4: ( s in A & t in A & s <> t ) ;
{s,t} c= A by ZFMISC_1:32, P4;
hence contradiction by p1, P4, LMThFRat32, ZMODUL02:56; :: thesis: verum

end;

end;