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