let R be RelStr ; 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; for C being Clique of R holds C /\ S is Clique of (subrelstr S)
let C be Clique of R; 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 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);
( 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
;
( not b in C /\ S or not a <> b or a <= b or b <= a )assume A4:
b in C /\ S
;
( not a <> b or a <= b or b <= a )assume A5:
a <> b
;
( 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;
verum end;
hence
C /\ S is Clique of (subrelstr S)
by Th6, A1, YELLOW_0:def 15; verum