set V = the Z_Module;
take (0). the Z_Module ; :: thesis: (0). the Z_Module is trivial
thus (0). the Z_Module is trivial ; :: thesis: verum