let R be with_finite_clique# RelStr ; :: thesis: for C being Clique of R
for S being Subset of R st card C = clique# R & C c= S holds
clique# (subrelstr S) = clique# R
let C be Clique of R; :: thesis: for S being Subset of R st card C = clique# R & C c= S holds
clique# (subrelstr S) = clique# R
let S be Subset of R; :: thesis: ( card C = clique# R & C c= S implies clique# (subrelstr S) = clique# R )
assume that
A: card C = clique# R and
B: C c= S ; :: thesis: clique# (subrelstr S) = clique# R
C = C /\ S by B, XBOOLE_1:28;
then C: C is Clique of (subrelstr S) by SPClique1;
consider Cs being Clique of (subrelstr S) such that
As: card Cs = clique# (subrelstr S) by Lheight;
D: card C <= card Cs by C, As, Lheight;
clique# (subrelstr S) <= clique# R by Hsubp0;
hence clique# (subrelstr S) = clique# R by As, A, D, XXREAL_0:1; :: thesis: verum