reconsider ZR = Rat-Module as divisible Z_Module ;
take ZR ; :: thesis: not ZR is trivial
reconsider v = 1 as Element of F_Rat ;
thus not ZR is trivial ; :: thesis: verum