set AG = INT.Ring ;
set G = Z_ModuleStruct(# the carrier of INT.Ring, the ZeroF of INT.Ring, the addF of INT.Ring,(Int-mult-left INT.Ring) #);
A1: Z_ModuleStruct(# the carrier of INT.Ring, the ZeroF of INT.Ring, the addF of INT.Ring,(Int-mult-left INT.Ring) #) is Z_Module by ZMODUL01:164;
not Z_ModuleStruct(# the carrier of INT.Ring, the ZeroF of INT.Ring, the addF 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