let A be finite set ; :: thesis:

hereby :: thesis:

assume A1: A is trivial ; :: thesis:

per cases ;

suppose A is empty ; :: thesis:

hence card A < 2 ; :: thesis:

end;

suppose not A is empty ; :: thesis:

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:

end;

end;

end;

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

per cases by A2, NAT_1:23;

suppose card A = 0 ; :: thesis:

hence A is trivial ; :: thesis:

end;

suppose card A = 1 ; :: thesis:

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

end;

end;