let A be finite set ; :: thesis: ( A is trivial iff card A < 2 )

hereby :: thesis: ( card A < 2 implies A is trivial )

assume A1: A is trivial ; :: thesis: card A < 2

per cases ( A is empty or not A is empty ) ;

suppose A is empty ; :: thesis: card A < 2

hence card A < 2 ; :: thesis: verum

end;

suppose not A is empty ; :: thesis: card A < 2

then ex x being object st A = {x} by A1, ZFMISC_1:131;
then card A = 1 by CARD_1:30;
hence card A < 2 ; :: thesis: verum

end;

end;

end;

assume A2: card A < 2 ; :: thesis: A is trivial

per cases ( card A = 0 or card A = 1 ) by A2, NAT_1:23;

suppose card A = 0 ; :: thesis: A is trivial

hence A is trivial ; :: thesis: verum

end;

suppose card A = 1 ; :: thesis: A is trivial

then A is 1 -element by CARD_1:def 7;
hence A is trivial ; :: thesis: verum

end;

end;