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