let G be trivial strict Group; :: thesis: (1). G = G
card G = 1 by Th12;
then card G = card ((1). G) by GROUP_2:81;
hence G = (1). G by GROUP_2:85; :: thesis: verum