let f be ConwayGameChain; :: thesis: for n, m being Element of dom f st n <= m holds
ConwayRank (f . n) c= ConwayRank (f . m)
let n, m be Element of dom f; :: thesis: ( n <= m implies ConwayRank (f . n) c= ConwayRank (f . m) )
assume A1: n <= m ; :: thesis: ConwayRank (f . n) c= ConwayRank (f . m)

per cases ( n < m or n = m ) by A1, XXREAL_0:1;

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

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

end;

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

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

end;

end;