let R be RelStr ; :: thesis: for S being Subset of R
for C being Clique of R holds C /\ S is Clique of (subrelstr S)
let S be Subset of R; :: thesis: for C being Clique of R holds C /\ S is Clique of (subrelstr S)
let C be Clique of R; :: thesis: C /\ S is Clique of (subrelstr S)
set sS = subrelstr S;
set CS = C /\ S;
Aa: C /\ S c= S by XBOOLE_1:17;
B: S = the carrier of (subrelstr S) by YELLOW_0:def 15;

now

let a, b be Element of (subrelstr S); :: thesis: ( not a in C /\ S or not b in C /\ S or not a <> b or a <= b or b <= a )
assume Z0: a in C /\ S ; :: thesis: ( not b in C /\ S or not a <> b or a <= b or b <= a )
assume Z1: b in C /\ S ; :: thesis: ( not a <> b or a <= b or b <= a )
assume Z2a: a <> b ; :: thesis: ( a <= b or b <= a )
ZZ: ( a in S & b in S ) by Z0, Z1, XBOOLE_0:def 4;
Z2: not S is empty by Z0;
not R is empty by Z0;
then reconsider a9 = a, b9 = b as Element of R by Z2, YELLOW_0:59;
( a9 in C & b9 in C ) by Z0, Z1, XBOOLE_0:def 4;
then ( a9 <= b9 or b9 <= a9 ) by Z2a, DClique;
hence ( a <= b or b <= a ) by ZZ, B, YELLOW_0:61; :: thesis: verum

end;

hence C /\ S is Clique of (subrelstr S) by DClique, Aa, YELLOW_0:def 15; :: thesis: verum