let S be set ; :: thesis: ( S is trivial implies S is finite )
assume A1: S is trivial ; :: thesis: S is finite

per cases ( S is empty or ex x being object st S = {x} ) by A1, ZFMISC_1:131;

suppose S is empty ; :: thesis: S is finite

hence S is finite ; :: thesis: verum

end;

suppose ex x being object st S = {x} ; :: thesis: S is finite

hence S is finite ; :: thesis: verum

end;

end;