defpred S2[ Ordinal] means for g being ConwayGame st g in ConwayDay $1 holds
not P1[g];
assume A2: for g being ConwayGame holds
( not P1[g] or ex g1 being ConwayGame st
( ConwayRank g1 in ConwayRank g & P1[g1] ) ) ; :: thesis: contradiction
A3: for alpha being Ordinal st ( for beta being Ordinal st beta in alpha holds
S2[beta] ) holds
S2[alpha]
proof
let alpha be Ordinal; :: thesis: ( ( for beta being Ordinal st beta in alpha holds
S2[beta] ) implies S2[alpha] )
assume A4: for beta being Ordinal st beta in alpha holds
S2[beta] ; :: thesis: S2[alpha]
let g be ConwayGame; :: thesis: ( g in ConwayDay alpha implies not P1[g] )
assume A5: ( g in ConwayDay alpha & P1[g] ) ; :: thesis: contradiction
then consider g1 being ConwayGame such that
A6: ( ConwayRank g1 in ConwayRank g & P1[g1] ) by A2;
ConwayRank g c= alpha by Th12, A5;
then consider beta being Ordinal such that
A7: ( beta in alpha & g1 in ConwayDay beta ) by Th13, A6;
thus contradiction by A4, A7, A6; :: thesis: verum
end;
A8: for alpha being Ordinal holds S2[alpha] from ORDINAL1:sch 2(A3);
 consider g being ConwayGame such that
A9: P1[g] by A1;
consider alpha being Ordinal such that
A10: g in ConwayDay alpha by Def3;
thus contradiction by A8, A9, A10; :: thesis: verum