let alpha be Ordinal; :: thesis: for g being ConwayGame holds
( g in ConwayDay alpha iff ConwayRank g c= alpha )
let g be ConwayGame; :: thesis: ( g in ConwayDay alpha iff ConwayRank g c= alpha )

hereby :: thesis: ( ConwayRank g c= alpha implies g in ConwayDay alpha )

assume A1: g in ConwayDay alpha ; :: thesis: ConwayRank g c= alpha
assume not ConwayRank g c= alpha ; :: thesis: contradiction
then alpha in ConwayRank g by ORDINAL1:16;
hence contradiction by A1, Def9; :: thesis: verum

end;

hereby :: thesis: verum

assume ConwayRank g c= alpha ; :: thesis: g in ConwayDay alpha
then A2: ConwayDay (ConwayRank g) c= ConwayDay alpha by Th3;
g in ConwayDay (ConwayRank g) by Def9;
hence g in ConwayDay alpha by A2; :: thesis: verum

end;