let G be trivial strict Group; :: thesis: (1). G = G
card G = 1 by Th11;
then card G = card ((1). G) by GROUP_2:69;
hence (1). G = G by GROUP_2:73; :: thesis: verum