for X being set
for M being Cardinal st X in M holds
card X in M by Th7, ORDINAL1:12;