take omega ; :: thesis: ( omega is Element of M & omega is cardinal & omega is infinite )
not M c= omega ;
hence omega is Element of M by ORDINAL1:16; :: thesis: ( omega is cardinal & omega is infinite )
thus ( omega is cardinal & omega is infinite ) ; :: thesis: verum