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