let alpha1, alpha2 be Ordinal; :: thesis: ( g in ConwayDay alpha1 & ( for beta being Ordinal st beta in alpha1 holds
not g in ConwayDay beta ) & g in ConwayDay alpha2 & ( for beta being Ordinal st beta in alpha2 holds
not g in ConwayDay beta ) implies alpha1 = alpha2 )
assume A5: ( g in ConwayDay alpha1 & ( for beta being Ordinal st beta in alpha1 holds
not g in ConwayDay beta ) ) ; :: thesis: ( not g in ConwayDay alpha2 or ex beta being Ordinal st
( beta in alpha2 & g in ConwayDay beta ) or alpha1 = alpha2 )
assume A6: ( g in ConwayDay alpha2 & ( for beta being Ordinal st beta in alpha2 holds
not g in ConwayDay beta ) ) ; :: thesis: alpha1 = alpha2
assume A7: alpha1 <> alpha2 ; :: thesis: contradiction

per cases ( alpha1 in alpha2 or alpha2 in alpha1 ) by A7, ORDINAL1:14;

suppose alpha1 in alpha2 ; :: thesis: contradiction

hence contradiction by A5, A6; :: thesis: verum

end;

suppose alpha2 in alpha1 ; :: thesis: contradiction

hence contradiction by A5, A6; :: thesis: verum

end;

end;