set ZR = Rat-Module ;
take Rat-Module ; :: thesis: Rat-Module is divisible
thus Rat-Module is divisible ; :: thesis: verum