take N ; :: thesis: N is N -element
thus card N = N by Def5; :: according to CARD_1:def 7 :: thesis: verum