theorem LMThFRat31: :: ZMODUL07:16

for s being Element of Rat-Module holds Lin {s} <> Rat-Module