theorem Th4: :: PENCIL_1:4

for X being set holds
( 2 c= card X iff not X is trivial )