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
A1: card C = clique# R and
A2: C c= S ; :: thesis: clique# (subrelstr S) = clique# R
C = C /\ S by A2, XBOOLE_1:28;
then A3: C is Clique of (subrelstr S) by Th29;
consider Cs being Clique of (subrelstr S) such that
A4: card Cs = clique# (subrelstr S) by Def4;
A5: card C <= card Cs by A3, A4, Def4;
clique# (subrelstr S) <= clique# R by Th42;
hence clique# (subrelstr S) = clique# R by A4, A1, A5, XXREAL_0:1; :: thesis: verum