let M be finite Cardinal; :: thesis: ex n being natural number st M = card n
card M = M by Def5;
hence ex n being natural number st M = card n ; :: thesis: verum