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
A1: card c = clique# (subrelstr S) by Def4;
c is Clique of R by Th28;
hence clique# (subrelstr S) <= clique# R by Def4, A1; :: thesis: verum