( ( 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 ) )