set AG = INT.Ring ;
set G = ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #);
A1: ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #) is Z_Module by ZMODUL01:164;
not ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #) is trivial ;
hence not for b₁ being Z_Module holds b₁ is trivial by A1; :: thesis: verum