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;
Z4:
not
R is
empty
by Z0;
reconsider a' =
a,
b' =
b as
Element of
R by Z2, Z4, YELLOW_0:59;
(
a' in C &
b' in C )
by Z0, Z1, XBOOLE_0:def 4;
then
(
a' <= b' or
b' <= a' )
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