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;