reconsider m = n as Element of NAT by ORDINAL1:def 12;
let x be Element of Rank n; :: thesis: x is finite
per cases ( Rank n = {} or Rank n <> {} ) ;
suppose Rank n = {} ; :: thesis: x is finite
hence x is finite ; :: thesis: verum
end;
suppose A1: Rank n <> {} ; :: thesis: x is finite
A2: Rank m is finite by CARD_2:67;
x c= Rank n by A1, ORDINAL1:def 2;
hence x is finite by A2; :: thesis: verum
end;
end;