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;