let k be Element of NAT ; for X being non empty set st 2 <= k & k + 2 c= card X holds
for K being Subset of the Points of (G_ (k,X)) st ( K is STAR or K is TOP ) holds
K is maximal_clique
let X be non empty set ; ( 2 <= k & k + 2 c= card X implies for K being Subset of the Points of (G_ (k,X)) st ( K is STAR or K is TOP ) holds
K is maximal_clique )
assume that
A1:
2 <= k
and
A2:
k + 2 c= card X
; for K being Subset of the Points of (G_ (k,X)) st ( K is STAR or K is TOP ) holds
K is maximal_clique
A3:
k - 2 is Element of NAT
by A1, NAT_1:21;
let K be Subset of the Points of (G_ (k,X)); ( ( K is STAR or K is TOP ) implies K is maximal_clique )
A4:
succ k = k + 1
by NAT_1:38;
A5:
succ (k + 1) = (k + 1) + 1
by NAT_1:38;
k + 1 <= k + 2
by XREAL_1:7;
then
k + 1 c= k + 2
by NAT_1:39;
then A6:
k + 1 c= card X
by A2, XBOOLE_1:1;
then A7:
the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k }
by A1, Def1;
A8:
the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 }
by A1, A6, Def1;
A9:
k - 1 is Element of NAT
by A1, NAT_1:21, XXREAL_0:2;
then A10:
succ (k - 1) = (k - 1) + 1
by NAT_1:38;
A11:
( K is STAR implies K is maximal_clique )
proof
assume
K is
STAR
;
K is maximal_clique
then consider S being
Subset of
X such that A12:
card S = k - 1
and A13:
K = { A where A is Subset of X : ( card A = k & S c= A ) }
by Def4;
A14:
S is
finite
by A1, A12, NAT_1:21, XXREAL_0:2;
A15:
for
U being
Subset of the
Points of
(G_ (k,X)) st
U is
clique &
K c= U holds
U = K
proof
A16:
succ (k - 2) = (k - 2) + 1
by A3, NAT_1:38;
let U be
Subset of the
Points of
(G_ (k,X));
( U is clique & K c= U implies U = K )
assume that A17:
U is
clique
and A18:
K c= U
and A19:
U <> K
;
contradiction
not
U c= K
by A18, A19, XBOOLE_0:def 10;
then consider A being
set such that A20:
A in U
and A21:
not
A in K
by TARSKI:def 3;
consider A2 being
POINT of
(G_ (k,X)) such that A22:
A2 = A
by A20;
card (S /\ A) c= k - 1
by A12, CARD_1:11, XBOOLE_1:17;
then
card (S /\ A) in succ (k - 1)
by A9, ORDINAL1:22;
then A23:
(
card (S /\ A) in succ (k - 2) or
card (S /\ A) = k - 1 )
by A16, ORDINAL1:8;
A24:
(
S /\ A c= S &
S /\ A c= A )
by XBOOLE_1:17;
A in the
Points of
(G_ (k,X))
by A20;
then A25:
ex
A1 being
Subset of
X st
(
A1 = A &
card A1 = k )
by A7;
then
not
S c= A
by A13, A21;
then A26:
card (S /\ A) c= k - 2
by A3, A12, A14, A24, A23, CARD_FIN:1, ORDINAL1:22;
A27:
not
X \ (A \/ S) <> {}
proof
A28:
succ (k - 2) = (k - 2) + 1
by A3, NAT_1:38;
assume
X \ (A \/ S) <> {}
;
contradiction
then consider y being
set such that A29:
y in X \ (A \/ S)
by XBOOLE_0:def 1;
A30:
not
y in A \/ S
by A29, XBOOLE_0:def 5;
then A31:
not
y in S
by XBOOLE_0:def 3;
then A32:
card (S \/ {y}) = (k - 1) + 1
by A12, A14, CARD_2:41;
A33:
{y} c= X
by A29, ZFMISC_1:31;
then
S \/ {y} c= X
by XBOOLE_1:8;
then
S \/ {y} in the
Points of
(G_ (k,X))
by A7, A32;
then consider B being
POINT of
(G_ (k,X)) such that A34:
B = S \/ {y}
;
A35:
not
y in A
by A30, XBOOLE_0:def 3;
A /\ B c= A /\ S
then
card (A /\ B) c= card (A /\ S)
by CARD_1:11;
then
card (A /\ B) c= k - 2
by A26, XBOOLE_1:1;
then A38:
card (A /\ B) in k - 1
by A3, A28, ORDINAL1:22;
A39:
for
L being
LINE of
(G_ (k,X)) holds not
{A2,B} on L
proof
A <> B
then A40:
k + 1
c= card (A \/ B)
by A25, A32, A34, Th1;
assume
ex
L being
LINE of
(G_ (k,X)) st
{A2,B} on L
;
contradiction
then consider L being
LINE of
(G_ (k,X)) such that A41:
{A2,B} on L
;
B on L
by A41, INCSP_1:1;
then A42:
B c= L
by A1, A6, Th10;
L in the
Lines of
(G_ (k,X))
;
then A43:
ex
L1 being
Subset of
X st
(
L = L1 &
card L1 = k + 1 )
by A8;
A2 on L
by A41, INCSP_1:1;
then
A c= L
by A1, A6, A22, Th10;
then
A \/ B c= L
by A42, XBOOLE_1:8;
then
card (A \/ B) c= k + 1
by A43, CARD_1:11;
then A44:
card (A \/ B) = (k - 1) + (2 * 1)
by A40, XBOOLE_0:def 10;
card B = (k - 1) + 1
by A12, A14, A31, A34, CARD_2:41;
then
card (A /\ B) = k - 1
by A9, A25, A44, Th2;
hence
contradiction
by A38;
verum
end;
A45:
S c= B
by A34, XBOOLE_1:7;
B c= X
by A33, A34, XBOOLE_1:8;
then
B in K
by A13, A32, A34, A45;
hence
contradiction
by A17, A18, A20, A22, A39, Def2;
verum
end;
k - 1
< (k - 1) + 1
by A9, NAT_1:13;
then
card S in card A
by A9, A12, A25, NAT_1:44;
then
A \ S <> {}
by CARD_1:68;
then consider x being
set such that A46:
x in A \ S
by XBOOLE_0:def 1;
not
x in S
by A46, XBOOLE_0:def 5;
then A47:
card (S \/ {x}) = (k - 1) + 1
by A12, A14, CARD_2:41;
A48:
{x} c= A
by A46, ZFMISC_1:31;
x in A
by A46;
then A49:
{x} c= X
by A25, ZFMISC_1:31;
then A50:
S \/ {x} c= X
by XBOOLE_1:8;
not
X \ (A \/ S) = {}
proof
assume
X \ (A \/ S) = {}
;
contradiction
then A51:
X c= A \/ S
by XBOOLE_1:37;
S \/ {x} in the
Points of
(G_ (k,X))
by A7, A47, A50;
then consider B being
POINT of
(G_ (k,X)) such that A52:
B = S \/ {x}
;
A \/ B = (A \/ S) \/ {x}
by A52, XBOOLE_1:4;
then A53:
A \/ B = A \/ S
by A48, XBOOLE_1:10, XBOOLE_1:12;
A \/ S c= X
by A25, XBOOLE_1:8;
then A54:
A \/ S = X
by A51, XBOOLE_0:def 10;
A55:
for
L being
LINE of
(G_ (k,X)) holds not
{A2,B} on L
proof
assume
ex
L being
LINE of
(G_ (k,X)) st
{A2,B} on L
;
contradiction
then consider L being
LINE of
(G_ (k,X)) such that A56:
{A2,B} on L
;
B on L
by A56, INCSP_1:1;
then A57:
B c= L
by A1, A6, Th10;
A2 on L
by A56, INCSP_1:1;
then
A c= L
by A1, A6, A22, Th10;
then
A \/ B c= L
by A57, XBOOLE_1:8;
then
card (A \/ B) c= card L
by CARD_1:11;
then A58:
k + 2
c= card L
by A2, A54, A53, XBOOLE_1:1;
L in the
Lines of
(G_ (k,X))
;
then
ex
L1 being
Subset of
X st
(
L = L1 &
card L1 = k + 1 )
by A8;
then
k + 1
in k + 1
by A5, A58, ORDINAL1:21;
hence
contradiction
;
verum
end;
(
S c= B &
B c= X )
by A49, A52, XBOOLE_1:8, XBOOLE_1:10;
then
B in K
by A13, A47, A52;
hence
contradiction
by A17, A18, A20, A22, A55, Def2;
verum
end;
hence
contradiction
by A27;
verum
end;
K is
clique
proof
let A,
B be
POINT of
(G_ (k,X));
COMBGRAS:def 2 ( A in K & B in K implies ex L being LINE of (G_ (k,X)) st {A,B} on L )
assume that A59:
A in K
and A60:
B in K
;
ex L being LINE of (G_ (k,X)) st {A,B} on L
A61:
ex
A1 being
Subset of
X st
(
A1 = A &
card A1 = k &
S c= A1 )
by A13, A59;
then A62:
A is
finite
;
A63:
ex
B1 being
Subset of
X st
(
B1 = B &
card B1 = k &
S c= B1 )
by A13, A60;
then
S c= A /\ B
by A61, XBOOLE_1:19;
then
k - 1
c= card (A /\ B)
by A12, CARD_1:11;
then
k - 1
in succ (card (A /\ B))
by A9, ORDINAL1:22;
then
(
card (A /\ B) = k - 1 or
k - 1
in card (A /\ B) )
by ORDINAL1:8;
then A64:
(
card (A /\ B) = k - 1 or
k c= card (A /\ B) )
by A10, ORDINAL1:21;
A65:
B is
finite
by A63;
A66:
(
card (A /\ B) = k implies ex
L being
LINE of
(G_ (k,X)) st
{A,B} on L )
proof
A67:
card A <> card X
card A c= card X
by A61, CARD_1:11;
then
card A in card X
by A67, CARD_1:3;
then
X \ A <> {}
by CARD_1:68;
then consider x being
set such that A68:
x in X \ A
by XBOOLE_0:def 1;
{x} c= X
by A68, ZFMISC_1:31;
then A69:
A \/ {x} c= X
by A61, XBOOLE_1:8;
not
x in A
by A68, XBOOLE_0:def 5;
then
card (A \/ {x}) = k + 1
by A61, A62, CARD_2:41;
then
A \/ {x} in the
Lines of
(G_ (k,X))
by A8, A69;
then consider L being
LINE of
(G_ (k,X)) such that A70:
L = A \/ {x}
;
assume
card (A /\ B) = k
;
ex L being LINE of (G_ (k,X)) st {A,B} on L
then
(
A /\ B = A &
A /\ B = B )
by A61, A63, A62, A65, CARD_FIN:1, XBOOLE_1:17;
then
B c= A \/ {x}
by XBOOLE_1:7;
then A71:
B on L
by A1, A6, A70, Th10;
A c= A \/ {x}
by XBOOLE_1:7;
then
A on L
by A1, A6, A70, Th10;
then
{A,B} on L
by A71, INCSP_1:1;
hence
ex
L being
LINE of
(G_ (k,X)) st
{A,B} on L
;
verum
end;
A72:
(
card (A /\ B) = k - 1 implies ex
L being
LINE of
(G_ (k,X)) st
{A,B} on L )
proof
A73:
A \/ B c= X
by A61, A63, XBOOLE_1:8;
assume A74:
card (A /\ B) = k - 1
;
ex L being LINE of (G_ (k,X)) st {A,B} on L
card A = (k - 1) + 1
by A61;
then
card (A \/ B) = (k - 1) + (2 * 1)
by A9, A63, A74, Th2;
then
A \/ B in the
Lines of
(G_ (k,X))
by A8, A73;
then consider L being
LINE of
(G_ (k,X)) such that A75:
L = A \/ B
;
B c= A \/ B
by XBOOLE_1:7;
then A76:
B on L
by A1, A6, A75, Th10;
A c= A \/ B
by XBOOLE_1:7;
then
A on L
by A1, A6, A75, Th10;
then
{A,B} on L
by A76, INCSP_1:1;
hence
ex
L being
LINE of
(G_ (k,X)) st
{A,B} on L
;
verum
end;
card (A /\ B) c= k
by A61, CARD_1:11, XBOOLE_1:17;
hence
ex
L being
LINE of
(G_ (k,X)) st
{A,B} on L
by A64, A72, A66, XBOOLE_0:def 10;
verum
end;
hence
K is
maximal_clique
by A15, Def3;
verum
end;
A77:
succ 0 = 0 + 1
;
( K is TOP implies K is maximal_clique )
proof
assume
K is
TOP
;
K is maximal_clique
then consider S being
Subset of
X such that A78:
card S = k + 1
and A79:
K = { A where A is Subset of X : ( card A = k & A c= S ) }
by Def5;
A80:
S is
finite
by A78;
A81:
for
U being
Subset of the
Points of
(G_ (k,X)) st
U is
clique &
K c= U holds
U = K
proof
A82:
k - 2
<= (k - 2) + 1
by A3, NAT_1:11;
let U be
Subset of the
Points of
(G_ (k,X));
( U is clique & K c= U implies U = K )
assume that A83:
U is
clique
and A84:
K c= U
and A85:
U <> K
;
contradiction
not
U c= K
by A84, A85, XBOOLE_0:def 10;
then consider A being
set such that A86:
A in U
and A87:
not
A in K
by TARSKI:def 3;
consider A2 being
POINT of
(G_ (k,X)) such that A88:
A2 = A
by A86;
A in the
Points of
(G_ (k,X))
by A86;
then A89:
ex
A1 being
Subset of
X st
(
A1 = A &
card A1 = k )
by A7;
then A90:
A is
finite
;
A91:
card A <> card S
by A78, A89;
A92:
not
A c= S
by A79, A87, A89;
then consider x being
set such that A93:
x in A
and A94:
not
x in S
by TARSKI:def 3;
k <= k + 1
by NAT_1:11;
then
card A c= card S
by A78, A89, NAT_1:39;
then
card A in card S
by A91, CARD_1:3;
then A95:
S \ A <> {}
by CARD_1:68;
2
c= card (S \ A)
then consider B1 being
set such that A98:
B1 c= S \ A
and A99:
card B1 = 2
by CARD_FIL:36;
A100:
B1 c= S
by A98, XBOOLE_1:106;
then A101:
not
x in B1
by A94;
card (S \ B1) = (k + 1) - 2
by A78, A80, A98, A99, CARD_2:44, XBOOLE_1:106;
then
k - 2
c= card (S \ B1)
by A3, A82, NAT_1:39;
then consider B2 being
set such that A102:
B2 c= S \ B1
and A103:
card B2 = k - 2
by A3, CARD_FIL:36;
A104:
card (B1 \/ B2) = 2
+ (k - 2)
by A80, A98, A99, A102, A103, CARD_2:40, XBOOLE_1:106;
A105:
B2 c= X
by A102, XBOOLE_1:1;
B1 c= X
by A98, XBOOLE_1:1;
then A106:
B1 \/ B2 c= X
by A105, XBOOLE_1:8;
then
B1 \/ B2 in the
Points of
(G_ (k,X))
by A7, A104;
then consider B being
POINT of
(G_ (k,X)) such that A107:
B = B1 \/ B2
;
B1 misses A
by A98, XBOOLE_1:106;
then A108:
B1 /\ A = {}
by XBOOLE_0:def 7;
B2 c= S
by A102, XBOOLE_1:106;
then A109:
B1 \/ B2 c= S
by A100, XBOOLE_1:8;
then A110:
not
x in B1 \/ B2
by A94;
A111:
A /\ B c= A \/ B
by XBOOLE_1:29;
A112:
k + 2
c= card (A \/ B)
proof
A113:
{x} \/ B1 misses A /\ B
{x} c= A
by A93, ZFMISC_1:31;
then
{x} c= A \/ B
by XBOOLE_1:10;
then A116:
(A /\ B) \/ {x} c= A \/ B
by A111, XBOOLE_1:8;
B1 c= B
by A107, XBOOLE_1:10;
then
B1 c= A \/ B
by XBOOLE_1:10;
then
((A /\ B) \/ {x}) \/ B1 c= A \/ B
by A116, XBOOLE_1:8;
then
(A /\ B) \/ ({x} \/ B1) c= A \/ B
by XBOOLE_1:4;
then A117:
card ((A /\ B) \/ ({x} \/ B1)) c= card (A \/ B)
by CARD_1:11;
assume
not
k + 2
c= card (A \/ B)
;
contradiction
then A118:
card (A \/ B) in succ (k + 1)
by A5, ORDINAL1:16;
then A119:
card (A \/ B) c= k + 1
by ORDINAL1:22;
(
card (A \/ B) = k + 1 or (
card (A \/ B) in succ k &
A c= A \/ B ) )
by A4, A118, ORDINAL1:8, XBOOLE_1:7;
then
(
card (A \/ B) = k + 1 or (
card (A \/ B) c= k &
k c= card (A \/ B) ) )
by A89, CARD_1:11, ORDINAL1:22;
then A120:
(
card (A \/ B) = (k - 1) + (2 * 1) or
card (A \/ B) = k + (2 * 0) )
by XBOOLE_0:def 10;
card A = (k - 1) + 1
by A89;
then A121:
(
card (A /\ B) = k - 1 or
card (A /\ B) = k )
by A9, A104, A107, A120, Th2;
card ({x} \/ B1) = 2
+ 1
by A80, A98, A99, A101, CARD_2:41;
then
(
card ((A /\ B) \/ ({x} \/ B1)) = (k - 1) + 3 or
card ((A /\ B) \/ ({x} \/ B1)) = k + 3 )
by A80, A90, A98, A113, A121, CARD_2:40;
then
(
k + 2
c= k + 1 or
k + 3
c= k + 1 )
by A119, A117, XBOOLE_1:1;
then
(
k + 1
in k + 1 or
k + 3
<= k + 1 )
by A5, NAT_1:39, ORDINAL1:21;
hence
contradiction
by XREAL_1:6;
verum
end;
A122:
for
L being
LINE of
(G_ (k,X)) holds not
{A2,B} on L
proof
assume
ex
L being
LINE of
(G_ (k,X)) st
{A2,B} on L
;
contradiction
then consider L being
LINE of
(G_ (k,X)) such that A123:
{A2,B} on L
;
B on L
by A123, INCSP_1:1;
then A124:
B c= L
by A1, A6, Th10;
L in the
Lines of
(G_ (k,X))
;
then A125:
ex
L1 being
Subset of
X st
(
L = L1 &
card L1 = k + 1 )
by A8;
A2 on L
by A123, INCSP_1:1;
then
A c= L
by A1, A6, A88, Th10;
then
A \/ B c= L
by A124, XBOOLE_1:8;
then A126:
card (A \/ B) c= k + 1
by A125, CARD_1:11;
k + 1
c= card (A \/ B)
by A89, A93, A104, A107, A110, Th1;
then
k + 2
c= k + 1
by A112, A126, XBOOLE_0:def 10;
then
k + 1
in k + 1
by A5, ORDINAL1:21;
hence
contradiction
;
verum
end;
B in K
by A79, A104, A106, A109, A107;
hence
contradiction
by A83, A84, A86, A88, A122, Def2;
verum
end;
K is
clique
proof
let A,
B be
POINT of
(G_ (k,X));
COMBGRAS:def 2 ( A in K & B in K implies ex L being LINE of (G_ (k,X)) st {A,B} on L )
assume that A127:
A in K
and A128:
B in K
;
ex L being LINE of (G_ (k,X)) st {A,B} on L
S in the
Lines of
(G_ (k,X))
by A8, A78;
then consider L being
LINE of
(G_ (k,X)) such that A129:
L = S
;
ex
B1 being
Subset of
X st
(
B1 = B &
card B1 = k &
B1 c= S )
by A79, A128;
then A130:
B on L
by A1, A6, A129, Th10;
ex
A1 being
Subset of
X st
(
A1 = A &
card A1 = k &
A1 c= S )
by A79, A127;
then
A on L
by A1, A6, A129, Th10;
then
{A,B} on L
by A130, INCSP_1:1;
hence
ex
L being
LINE of
(G_ (k,X)) st
{A,B} on L
;
verum
end;
hence
K is
maximal_clique
by A81, Def3;
verum
end;
hence
( ( K is STAR or K is TOP ) implies K is maximal_clique )
by A11; verum