let R be RelStr ; :: thesis: for S being Subset of R
for C being Clique of (subrelstr S) holds C is Clique of R
let S be Subset of R; :: thesis: for C being Clique of (subrelstr S) holds C is Clique of R
let C be Clique of (subrelstr S); :: thesis: C is Clique of R
A1: the carrier of (subrelstr S) = S by YELLOW_0:def 15;
now :: thesis: for a, b being Element of R st a in C & b in C & a <> b & not a <= b holds
b <= a
let a, b be Element of R; :: thesis: ( a in C & b in C & a <> b & not a <= b implies b <= a )
assume that
A2: a in C and
A3: b in C and
A4: a <> b ; :: thesis: ( a <= b or b <= a )
reconsider a9 = a, b9 = b as Element of (subrelstr S) by A2, A3;
( a9 <= b9 or b9 <= a9 ) by A2, A3, A4, Th6;
hence ( a <= b or b <= a ) by YELLOW_0:59; :: thesis: verum
end;
hence C is Clique of R by A1, Th6, XBOOLE_1:1; :: thesis: verum