defpred S₂[ Ordinal] means g in ConwayDay $1;
A2: ex alpha being Ordinal st S₂[alpha] by Def3, A1;
consider alpha being Ordinal such that
A3: ( S₂[alpha] & ( for beta being Ordinal st S₂[beta] holds
alpha c= beta ) ) from ORDINAL1:sch 1(A2);
take alpha ; :: thesis: ( g in ConwayDay alpha & ( for beta being Ordinal st beta in alpha holds
not g in ConwayDay beta ) )
thus g in ConwayDay alpha by A3; :: thesis: for beta being Ordinal st beta in alpha holds
not g in ConwayDay beta
let beta be Ordinal; :: thesis: ( beta in alpha implies not g in ConwayDay beta )
assume A4: beta in alpha ; :: thesis: not g in ConwayDay beta
assume g in ConwayDay beta ; :: thesis: contradiction
then alpha c= beta by A3;
then beta in beta by A4;
hence contradiction ; :: thesis: verum