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;

thus ( ex beta being Ordinal st
( beta in alpha & g in ConwayDay beta ) implies ConwayRank g in alpha ) by Th12, ORDINAL1:12; :: thesis: verum