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;