scheme :: CARD_1:sch 2
CardinalCompInd{ P1[ set ] } :
for M being Cardinal holds P1[M]
provided
A1: for M being Cardinal st ( for N being Cardinal st N in M holds
P1[N] ) holds
P1[M]