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