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

per cases ( S is empty or ex x being set st S = {x} ) by A2, REALSET1:def 4;

suppose S is empty ; :: thesis: contradiction

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

end;

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

hence contradiction by A1; :: thesis: verum

end;

end;