let alpha be Ordinal; :: thesis: for g being ConwayGame holds
( ConwayRank g in alpha iff ex beta being Ordinal st
( beta in alpha & g in ConwayDay beta ) )
let g be ConwayGame; :: thesis: ( ConwayRank g in alpha iff ex beta being Ordinal st
( beta in alpha & g in ConwayDay beta ) )

hereby :: thesis: ( ex beta being Ordinal st
( beta in alpha & g in ConwayDay beta ) implies ConwayRank g in alpha )

assume A1: ConwayRank g in alpha ; :: thesis: ex beta being Ordinal st
( beta in alpha & g in ConwayDay beta )
take beta = ConwayRank g; :: thesis: ( beta in alpha & g in ConwayDay beta )
thus beta in alpha by A1; :: thesis: g in ConwayDay beta
thus g in ConwayDay beta by Th12; :: thesis: verum

end;

hereby :: thesis: verum

assume ex beta being Ordinal st
( beta in alpha & g in ConwayDay beta ) ; :: thesis: ConwayRank g in alpha
then consider beta being Ordinal such that
A2: ( beta in alpha & g in ConwayDay beta ) ;
ConwayRank g c= beta by Th12, A2;
hence ConwayRank g in alpha by A2, ORDINAL1:22; :: thesis: verum

end;