theorem Th11: :: GROUP_6:11

( ( for G being trivial Group holds
( card G = 1 & G is finite ) ) & ( for G being finite Group st card G = 1 holds
G is trivial ) )