let B be Element of A; :: thesis: B is finite

per cases ( A is empty or not A is empty ) ;

suppose A is empty ; :: thesis: B is finite

hence B is finite by SUBSET_1:def 1; :: thesis: verum

end;

suppose not A is empty ; :: thesis: B is finite

hence B is finite by Def6; :: thesis: verum

end;

end;