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

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

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

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

end;

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

hence e is finite ; :: thesis: verum

end;

end;