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 set st S = {x} ) by A1, Def4;

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

then reconsider T = S as empty set ;
T is finite ;
hence S is finite ; :: thesis: verum

end;

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

hence S is finite ; :: thesis: verum

end;

end;