let R be with_finite_chromatic# RelStr ; :: thesis: for S being Subset of R holds chromatic# R >= chromatic# (subrelstr S)
let S be Subset of R; :: thesis: chromatic# R >= chromatic# (subrelstr S)
consider C being finite Coloring of R such that
A1: card C = chromatic# R by Def3;
C | S is Coloring of (subrelstr S) by Th10;
then A2: card (C | S) >= chromatic# (subrelstr S) by Def3;
card C >= card (C | S) by Th8;
hence chromatic# R >= chromatic# (subrelstr S) by A1, A2, XXREAL_0:2; :: thesis: verum