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;
A1: C /\ S c= S by XBOOLE_1:17;
A2: S = the carrier of (subrelstr S) by YELLOW_0:def 15;

now :: thesis: for a, b being Element of (subrelstr S) holds
( not a in C /\ S or not b in C /\ S or not a <> b or a <= b or b <= a )

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 A3: a in C /\ S ; :: thesis: ( not b in C /\ S or not a <> b or a <= b or b <= a )
assume A4: b in C /\ S ; :: thesis: ( not a <> b or a <= b or b <= a )
assume A5: a <> b ; :: thesis: ( a <= b or b <= a )
A6: ( a in S & b in S ) by A3, A4, XBOOLE_0:def 4;
A7: not S is empty by A3;
not R is empty by A3;
then reconsider a9 = a, b9 = b as Element of R by A7, YELLOW_0:58;
( a9 in C & b9 in C ) by A3, A4, XBOOLE_0:def 4;
then ( a9 <= b9 or b9 <= a9 ) by A5, Th6;
hence ( a <= b or b <= a ) by A6, A2, YELLOW_0:60; :: thesis: verum

end;

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