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