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

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

hence Involved A is finite by Lm2; :: thesis: verum

end;

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

hence Involved A is finite by Th7; :: thesis: verum

end;

end;