per cases ( X is empty or not X is empty ) ;
suppose X is empty ; :: thesis: card X is trivial
hence card X is trivial ; :: thesis: verum
end;
suppose not X is empty ; :: thesis: card X is trivial
then consider x being object such that
A1: X = {x} by ZFMISC_1:131;
thus card X is trivial by A1, CARD_1:30, CARD_1:49; :: thesis: verum
end;
end;