let f be ConwayGameChain; :: thesis:
let n, m be Element of dom f; :: thesis:
assume A1: n <= m ; :: thesis:

per cases by A1, XXREAL_0:1;

suppose n < m ; :: thesis:

then ConwayRank (f . n) in ConwayRank (f . m) by Th21;
hence ConwayRank (f . n) c= ConwayRank (f . m) by ORDINAL1:def 2; :: thesis:

end;

suppose n = m ; :: thesis:

hence ConwayRank (f . n) c= ConwayRank (f . m) ; :: thesis:

end;

end;