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

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

assume A is trivial ; :: thesis: card A < 2
then A1: ( A is empty or ex x being set st A = {x} ) by Def4;

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

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

hence card A < 2 by CARD_1:47; :: thesis: verum

end;

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

then card A = 1 by A1, CARD_1:50;
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 empty or ex x being set st A = {x} ) ; :: according to REALSET1:def 4 :: thesis: verum

end;

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

hence ( A is empty or ex x being set st A = {x} ) by CARD_2:60; :: according to REALSET1:def 4 :: thesis: verum

end;

end;