let R be with_finite_clique# RelStr ; :: thesis: for S being Subset of R holds clique# (subrelstr S) <= clique# R
let S be Subset of R; :: thesis: clique# (subrelstr S) <= clique# R
set s = subrelstr S;
consider c being finite Clique of (subrelstr S) such that
a: card c = clique# (subrelstr S) by Lheight;
c is Clique of R by SPClique;
hence clique# (subrelstr S) <= clique# R by Lheight, a; :: thesis: verum