let e be Singleton of E; :: thesis: e is finite

per cases ( e is empty or ex x being set st e = {x} ) by ZFMISC_1:131;

suppose e is empty ; :: thesis: e is finite

then reconsider T = e as empty set ;
thus e is finite ; :: thesis: verum

end;

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

thus e is finite ; :: thesis: verum

end;

end;