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
A: card C = chromatic# R by Lchro;
C | S is Coloring of (subrelstr S) by Tsr0;
then B: card (C | S) >= chromatic# (subrelstr S) by Lchro;
card C >= card (C | S) by Tpart0;
hence chromatic# R >= chromatic# (subrelstr S) by A, B, XXREAL_0:2; :: thesis: verum