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;