theorem :: NAT_D:60

for A being finite set holds
( A is trivial iff card A < 2 )