let M be finite Cardinal; :: thesis: ex n being Nat st M = card n
card M = M by Def2;
hence ex n being Nat st M = card n ; :: thesis: verum