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