set G = the addGroup;
take (0). the addGroup ; :: thesis: ( (0). the addGroup is strict & (0). the addGroup is finite )
thus ( (0). the addGroup is strict & (0). the addGroup is finite ) ; :: thesis: verum