let k be Element of NAT ; :: thesis: 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) holds
( not K is maximal_clique or K is STAR or K is TOP )
let X be non empty set ; :: thesis: ( 2 <= k & k + 2 c= card X implies for K being Subset of the Points of (G_ k,X) holds
( not K is maximal_clique or K is STAR or K is TOP ) )
assume A1:
( 2 <= k & k + 2 c= card X )
; :: thesis: for K being Subset of the Points of (G_ k,X) holds
( not K is maximal_clique or K is STAR or K is TOP )
then A2:
( k - 2 is Element of NAT & k + 1 <= k + 2 & 1 <= k )
by NAT_1:21, XREAL_1:9, XXREAL_0:2;
then A3:
( - 2 < 0 & k + 1 c= k + 2 )
by NAT_1:40;
then A4:
( 2 - 2 < k & k + 1 c= card X )
by A1, XBOOLE_1:1;
A5:
k - 1 is Element of NAT
by A2, NAT_1:21;
A6:
the Points of (G_ k,X) = { A where A is Subset of X : card A = k }
by A4, Def1;
A7:
the Lines of (G_ k,X) = { L where L is Subset of X : card L = k + 1 }
by A4, Def1;
let K be Subset of the Points of (G_ k,X); :: thesis: ( not K is maximal_clique or K is STAR or K is TOP )
A8:
( succ (k - 1) = (k - 1) + 1 & succ k = k + 1 & succ (k + 1) = (k + 1) + 1 & card k = k & card (k - 1) = k - 1 & card 2 = 2 & card 1 = 1 & card 0 = 0 & succ 1 = 1 + 1 & succ 0 = 0 + 1 & card (k + 1) = k + 1 & card (k - 2) = k - 2 & succ (k - 2) = (k - 2) + 1 & succ 2 = 2 + 1 )
by A2, A5, CARD_1:def 5, NAT_1:39;
assume A9:
K is maximal_clique
; :: thesis: ( K is STAR or K is TOP )
then A10:
( K is clique & k <= k + 1 )
by Def3, NAT_1:11;
then A11:
k c= k + 1
by NAT_1:40;
then A12:
( k c= card X & K is Subset of the Points of (G_ k,X) )
by A4, XBOOLE_1:1;
A13:
K <> {}
proof
assume A14:
K = {}
;
:: thesis: contradiction
consider A1 being
set such that A15:
(
A1 c= X &
card A1 = k )
by A12, CARD_FIL:36;
A1 in the
Points of
(G_ k,X)
by A6, A15;
then consider A being
POINT of
(G_ k,X) such that A16:
A = A1
;
card A <> card X
then
card A in card X
by A12, A15, A16, CARD_1:13;
then
X \ A <> {}
by CARD_2:4;
then consider x being
set such that A17:
x in X \ A
by XBOOLE_0:def 1;
A18:
(
x in X & not
x in A &
A is
finite )
by A15, A16, A17, XBOOLE_0:def 5;
{x} c= X
by A17, ZFMISC_1:37;
then
(
card (A \/ {x}) = k + 1 &
A \/ {x} c= X )
by A15, A16, A18, CARD_2:54, XBOOLE_1:8;
then
A \/ {x} in the
Lines of
(G_ k,X)
by A7;
then consider L being
LINE of
(G_ k,X) such that A19:
L = A \/ {x}
;
A c= L
by A19, XBOOLE_1:7;
then A20:
A on L
by A4, Th10;
consider U being
Subset of the
Points of
(G_ k,X) such that A21:
U = {A}
;
A22:
K c= U
by A14, XBOOLE_1:2;
U is
clique
proof
let B,
C be
POINT of
(G_ k,X);
:: according to COMBGRAS:def 2 :: thesis: ( B in U & C in U implies ex L being LINE of (G_ k,X) st {B,C} on L )
assume
(
B in U &
C in U )
;
:: thesis: ex L being LINE of (G_ k,X) st {B,C} on L
then
(
B on L &
C on L )
by A20, A21, TARSKI:def 1;
then
{B,C} on L
by INCSP_1:11;
hence
ex
L being
LINE of
(G_ k,X) st
{B,C} on L
;
:: thesis: verum
end;
hence
contradiction
by A9, A14, A21, A22, Def3;
:: thesis: verum
end;
A23:
card K <> 1
proof
assume
card K = 1
;
:: thesis: contradiction
then consider A3 being
set such that A24:
K = {A3}
by CARD_2:60;
A25:
A3 in K
by A24, TARSKI:def 1;
then A26:
A3 in the
Points of
(G_ k,X)
;
consider A being
POINT of
(G_ k,X) such that A27:
A = A3
by A25;
consider A4 being
Subset of
X such that A28:
(
A = A4 &
card A4 = k )
by A6, A26, A27;
A29:
card A c= card X
by A4, A11, A28, XBOOLE_1:1;
card A <> card X
then
card A in card X
by A29, CARD_1:13;
then
X \ A <> {}
by CARD_2:4;
then consider x being
set such that A30:
x in X \ A
by XBOOLE_0:def 1;
A31:
(
x in X & not
x in A &
A is
finite )
by A28, A30, XBOOLE_0:def 5;
A32:
{x} c= X
by A30, ZFMISC_1:37;
then
(
card (A \/ {x}) = k + 1 &
A \/ {x} c= X )
by A28, A31, CARD_2:54, XBOOLE_1:8;
then
A \/ {x} in the
Lines of
(G_ k,X)
by A7;
then consider L being
LINE of
(G_ k,X) such that A33:
L = A \/ {x}
;
A34:
A c= L
by A33, XBOOLE_1:7;
then A35:
A on L
by A4, Th10;
k - 1
<= (k - 1) + 1
by A5, NAT_1:11;
then
k - 1
c= card A
by A5, A28, NAT_1:40;
then consider B2 being
set such that A36:
(
B2 c= A &
card B2 = k - 1 )
by A5, CARD_FIL:36;
(
B2 c= X & not
x in B2 &
B2 is
finite )
by A5, A28, A30, A36, XBOOLE_0:def 5, XBOOLE_1:1;
then
(
card (B2 \/ {x}) = (k - 1) + 1 &
B2 \/ {x} c= X )
by A32, A36, CARD_2:54, XBOOLE_1:8;
then
B2 \/ {x} in the
Points of
(G_ k,X)
by A6;
then consider A1 being
POINT of
(G_ k,X) such that A37:
A1 = B2 \/ {x}
;
(
B2 c= L &
{x} c= L )
by A33, A34, A36, XBOOLE_1:1, XBOOLE_1:7;
then
A1 c= L
by A37, XBOOLE_1:8;
then A38:
A1 on L
by A4, Th10;
A39:
A <> A1
consider U being
Subset of the
Points of
(G_ k,X) such that A40:
U = {A,A1}
;
A in U
by A40, TARSKI:def 2;
then A41:
K c= U
by A24, A27, ZFMISC_1:37;
A42:
U is
clique
proof
let B1,
B2 be
POINT of
(G_ k,X);
:: according to COMBGRAS:def 2 :: thesis: ( B1 in U & B2 in U implies ex L being LINE of (G_ k,X) st {B1,B2} on L )
assume
(
B1 in U &
B2 in U )
;
:: thesis: ex L being LINE of (G_ k,X) st {B1,B2} on L
then
(
B1 on L &
B2 on L )
by A35, A38, A40, TARSKI:def 2;
then
{B1,B2} on L
by INCSP_1:11;
hence
ex
L being
LINE of
(G_ k,X) st
{B1,B2} on L
;
:: thesis: verum
end;
U <> K
hence
contradiction
by A9, A41, A42, Def3;
:: thesis: verum
end;
0 c= card K
by XBOOLE_1:2;
then
0 in succ (card K)
by ORDINAL1:34;
then
( card K = 0 or 0 in card K )
by ORDINAL1:13;
then
1 c= card K
by A8, A13, ORDINAL1:33;
then
1 in succ (card K)
by ORDINAL1:34;
then
( card K = 1 or 1 in card K )
by ORDINAL1:13;
then A43:
2 c= card K
by A8, A23, ORDINAL1:33;
then consider R being set such that
A44:
( R c= K & card R = 2 )
by CARD_FIL:36;
R is finite
by A44;
then consider A1, B1 being set such that
A45:
( A1 <> B1 & R = {A1,B1} )
by A44, CARD_2:79;
A46:
( A1 in R & B1 in R )
by A45, TARSKI:def 2;
then A47:
( A1 in the Points of (G_ k,X) & B1 in the Points of (G_ k,X) )
by A44, TARSKI:def 3;
then consider A being POINT of (G_ k,X) such that
A48:
A = A1
;
consider B being POINT of (G_ k,X) such that
A49:
B = B1
by A47;
consider A2 being Subset of X such that
A50:
( A2 = A & card A2 = k )
by A6, A47, A48;
consider B2 being Subset of X such that
A51:
( B2 = B & card B2 = k )
by A6, A47, A49;
consider L being LINE of (G_ k,X) such that
A52:
{A,B} on L
by A10, A44, A46, A48, A49, Def2;
( A on L & B on L )
by A52, INCSP_1:11;
then A53:
( A c= L & B c= L )
by A4, Th10;
A54:
( A is finite & B is finite )
by A50, A51;
L in the Lines of (G_ k,X)
;
then consider L1 being Subset of X such that
A55:
( L1 = L & card L1 = k + 1 )
by A7;
A56:
( A \/ B c= L & A /\ B c= L & L is finite )
by A53, A55, XBOOLE_1:8, XBOOLE_1:108;
then A57:
( card (A \/ B) c= k + 1 & k + 1 c= card (A \/ B) )
by A45, A48, A49, A50, A51, A55, Th1, CARD_1:27;
then A58:
( card (A \/ B) = k + 1 & A /\ B c= X & A \/ B is finite )
by A55, A56, XBOOLE_0:def 10, XBOOLE_1:1;
then A59:
A \/ B = L
by A55, A56, CARD_FIN:1;
A60:
( ex C being POINT of (G_ k,X) st
( C in K & C on L & A <> C & B <> C ) implies K is TOP )
proof
assume
ex
C being
POINT of
(G_ k,X) st
(
C in K &
C on L &
A <> C &
B <> C )
;
:: thesis: K is TOP
then consider C being
POINT of
(G_ k,X) such that A61:
(
C in K &
C on L &
A <> C &
B <> C )
;
A62:
C c= L
by A4, A61, Th10;
C in the
Points of
(G_ k,X)
;
then consider C2 being
Subset of
X such that A63:
(
C2 = C &
card C2 = k )
by A6;
A64:
(
A \/ C c= L &
B \/ C c= L &
C is
finite &
L is
finite )
by A53, A55, A62, A63, XBOOLE_1:8;
then A65:
(
(A \/ B) \/ C c= L &
card (A \/ C) c= k + 1 &
k + 1
c= card (A \/ C) &
A \/ B is
finite &
card (B \/ C) c= k + 1 &
k + 1
c= card (B \/ C) )
by A50, A51, A55, A56, A61, A62, A63, Th1, CARD_1:27, XBOOLE_1:8;
then A66:
(
card (A \/ B) = (k - 1) + (2 * 1) &
card (B \/ C) = (k - 1) + (2 * 1) &
A \/ B c= (A \/ B) \/ C &
card (A \/ C) = (k - 1) + (2 * 1) &
card A = (k - 1) + 1 &
card B = (k - 1) + 1 &
card C = (k - 1) + 1 )
by A50, A51, A57, A63, XBOOLE_0:def 10, XBOOLE_1:7;
then
(
card (A /\ B) = k - 1 &
card (B /\ C) = k - 1 &
A \/ B = L &
card (A /\ C) = k - 1 &
A \/ B c= (A \/ B) \/ C )
by A5, A55, A56, Th2, CARD_FIN:1;
then A67:
(
card ((A \/ B) \/ C) = k + 1 &
card A = (k + 1) - 1 &
card B = (k + 1) - 1 &
card C = (k + 1) - 1 &
card (A /\ C) = (k + 1) - 2 & 2
+ 1
<= k + 1 &
card (B /\ C) = (k + 1) - 2 &
card (A /\ B) = (k + 1) - 2 & 1
+ 1
<= k + 1 )
by A1, A2, A65, A66, XBOOLE_0:def 10, XREAL_1:9;
then A68:
( (
card ((A /\ B) /\ C) = (k + 1) - 3 &
card ((A \/ B) \/ C) = k + 1 ) or (
card ((A /\ B) /\ C) = (k + 1) - 2 &
card ((A \/ B) \/ C) = (k + 1) + 1 ) )
by Th7;
consider T being
set such that A69:
T = { D where D is Subset of X : ( card D = k & D c= L ) }
;
A70:
K c= T
proof
let D2 be
set ;
:: according to TARSKI:def 3 :: thesis: ( not D2 in K or D2 in T )
assume A71:
(
D2 in K & not
D2 in T )
;
:: thesis: contradiction
then
D2 in the
Points of
(G_ k,X)
;
then consider D1 being
Subset of
X such that A72:
(
D1 = D2 &
card D1 = k )
by A6;
consider D being
POINT of
(G_ k,X) such that A73:
D = D1
by A71, A72;
not
D c= L
by A69, A71, A72, A73;
then consider x being
set such that A74:
(
x in D & not
x in L )
by TARSKI:def 3;
consider L11 being
LINE of
(G_ k,X) such that A75:
{A,D} on L11
by A10, A44, A46, A48, A71, A72, A73, Def2;
consider L12 being
LINE of
(G_ k,X) such that A76:
{B,D} on L12
by A10, A44, A46, A49, A71, A72, A73, Def2;
consider L13 being
LINE of
(G_ k,X) such that A77:
{C,D} on L13
by A10, A61, A71, A72, A73, Def2;
L11 in the
Lines of
(G_ k,X)
;
then consider L21 being
Subset of
X such that A78:
(
L21 = L11 &
card L21 = k + 1 )
by A7;
L12 in the
Lines of
(G_ k,X)
;
then consider L22 being
Subset of
X such that A79:
(
L22 = L12 &
card L22 = k + 1 )
by A7;
L13 in the
Lines of
(G_ k,X)
;
then consider L23 being
Subset of
X such that A80:
(
L23 = L13 &
card L23 = k + 1 )
by A7;
A81:
(
A <> D &
B <> D &
C <> D )
by A53, A62, A69, A71, A72, A73;
(
A on L11 &
D on L11 &
B on L12 &
D on L12 &
C on L13 &
D on L13 )
by A75, A76, A77, INCSP_1:11;
then
(
A c= L11 &
D c= L11 &
B c= L12 &
D c= L12 &
C c= L13 &
D c= L13 )
by A4, Th10;
then
(
A \/ D c= L11 &
B \/ D c= L12 &
C \/ D c= L13 )
by XBOOLE_1:8;
then
(
card (A \/ D) c= k + 1 &
card (B \/ D) c= k + 1 &
card (C \/ D) c= k + 1 &
k + 1
c= card (A \/ D) &
k + 1
c= card (B \/ D) &
k + 1
c= card (C \/ D) )
by A50, A51, A63, A72, A73, A78, A79, A80, A81, Th1, CARD_1:27;
then A82:
(
card A = (k - 1) + 1 &
card B = (k - 1) + 1 &
card C = (k - 1) + 1 &
card D = (k - 1) + 1 &
card (A \/ D) = (k - 1) + (2 * 1) &
card (B \/ D) = (k - 1) + (2 * 1) &
card (C \/ D) = (k - 1) + (2 * 1) )
by A50, A51, A63, A72, A73, XBOOLE_0:def 10;
then A83:
(
card (A /\ D) = k - 1 &
card (B /\ D) = k - 1 &
card (C /\ D) = k - 1 &
{x} c= D &
D is
finite &
card {x} = 1 &
D \ {x} c= D &
A /\ D is
finite &
B /\ D is
finite &
C /\ D is
finite )
by A5, A54, A64, A74, Th2, CARD_1:50, ZFMISC_1:37;
then A84:
(
card (D \ {x}) = k - 1 &
D \ {x} is
finite & not
x in A & not
x in B & not
x in C )
by A53, A62, A72, A73, A74, CARD_2:63;
A85:
A /\ D c= D \ {x}
A87:
B /\ D c= D \ {x}
C /\ D c= D \ {x}
then A90:
(
A /\ D = D \ {x} &
B /\ D = D \ {x} &
C /\ D = D \ {x} )
by A83, A84, A85, A87, CARD_FIN:1;
then
A /\ D = (A /\ D) /\ (B /\ D)
;
then
A /\ D = (A /\ (D /\ B)) /\ D
by XBOOLE_1:16;
then
A /\ D = ((A /\ B) /\ D) /\ D
by XBOOLE_1:16;
then
A /\ D = (A /\ B) /\ (D /\ D)
by XBOOLE_1:16;
then
A /\ D = ((A /\ B) /\ D) /\ (C /\ D)
by A90;
then
A /\ D = ((A /\ B) /\ (D /\ C)) /\ D
by XBOOLE_1:16;
then
A /\ D = (((A /\ B) /\ C) /\ D) /\ D
by XBOOLE_1:16;
then
A /\ D = ((A /\ B) /\ C) /\ (D /\ D)
by XBOOLE_1:16;
then
(
card (((A /\ B) /\ C) /\ D) = k - 1 &
((A /\ B) /\ C) /\ D c= (A /\ B) /\ C )
by A5, A82, Th2, XBOOLE_1:17;
then
k - 1
c= k - 2
by A67, A68, CARD_1:27;
then
k - 1
in k - 1
by A8, ORDINAL1:34;
hence
contradiction
;
:: thesis: verum
end;
T c= the
Points of
(G_ k,X)
then consider T1 being
Subset of the
Points of
(G_ k,X) such that A92:
T1 = T
;
A93:
T1 is
TOP
by A55, A69, A92, Def5;
then
T1 is
maximal_clique
by A1, Th14;
then
T1 is
clique
by Def3;
hence
K is
TOP
by A9, A70, A92, A93, Def3;
:: thesis: verum
end;
( ( for C being POINT of (G_ k,X) holds
( not C in K or not C on L or not A <> C or not B <> C ) ) implies K is STAR )
proof
assume A94:
for
C being
POINT of
(G_ k,X) holds
( not
C in K or not
C on L or not
A <> C or not
B <> C )
;
:: thesis: K is STAR
A95:
(
card A = (k - 1) + 1 &
card B = (k - 1) + 1 &
card (A \/ B) = (k - 1) + (2 * 1) )
by A50, A51, A57, XBOOLE_0:def 10;
then A96:
card (A /\ B) = k - 1
by A5, Th2;
consider S being
set such that A97:
S = { D where D is Subset of X : ( card D = k & A /\ B c= D ) }
;
A98:
card L c= card X
by A1, A3, A55, XBOOLE_1:1;
card L <> card X
then
card L in card X
by A98, CARD_1:13;
then
X \ L <> {}
by CARD_2:4;
then consider x being
set such that A99:
x in X \ L
by XBOOLE_0:def 1;
A100:
(
{x} c= X & not
x in A /\ B & not
x in A & not
x in B &
A /\ B is
finite )
by A53, A56, A99, XBOOLE_0:def 5, ZFMISC_1:37;
then A101:
(
card ((A /\ B) \/ {x}) = (k - 1) + 1 &
(A /\ B) \/ {x} c= X )
by A58, A96, CARD_2:54, XBOOLE_1:8;
then
(A /\ B) \/ {x} in the
Points of
(G_ k,X)
by A6;
then consider C being
POINT of
(G_ k,X) such that A102:
C = (A /\ B) \/ {x}
;
A103:
(
A /\ {x} = {} &
B /\ {x} = {} )
A105:
(
A /\ B c= C &
A /\ B c= A &
A /\ B c= B )
by A102, XBOOLE_1:7, XBOOLE_1:17;
(
A /\ C = (A /\ {x}) \/ (A /\ (A /\ B)) &
B /\ C = (B /\ {x}) \/ (B /\ (B /\ A)) )
by A102, XBOOLE_1:23;
then A106:
(
A /\ C = (A /\ {x}) \/ ((A /\ A) /\ B) &
B /\ C = (B /\ {x}) \/ ((B /\ B) /\ A) )
by XBOOLE_1:16;
A107:
(
card A = (k - 1) + 1 &
card B = (k - 1) + 1 &
card (A \/ B) = (k - 1) + (2 * 1) )
by A50, A51, A57, XBOOLE_0:def 10;
then A108:
(
card (A /\ B) = k - 1 &
A c= A \/ B &
B c= B \/ C &
C c= A \/ C )
by A5, Th2, XBOOLE_1:7;
(
card (A /\ C) = k - 1 &
card (B /\ C) = k - 1 )
by A5, A103, A106, A107, Th2;
then A109:
(
card (A \/ C) = (k - 1) + (2 * 1) &
card (B \/ C) = (k - 1) + (2 * 1) &
A \/ C c= X &
B \/ C c= X &
C is
finite )
by A5, A50, A51, A101, A102, Th2, XBOOLE_1:8;
then
A \/ C in the
Lines of
(G_ k,X)
by A7;
then consider L1 being
LINE of
(G_ k,X) such that A110:
L1 = A \/ C
;
B \/ C in the
Lines of
(G_ k,X)
by A7, A109;
then consider L2 being
LINE of
(G_ k,X) such that A111:
L2 = B \/ C
;
A112:
(
A /\ B is
finite &
A /\ C is
finite &
B /\ C is
finite &
C is
finite )
by A54, A102;
A113:
(
card (A \ (A /\ B)) = k - (k - 1) &
card (B \ (A /\ B)) = k - (k - 1) )
by A50, A51, A54, A105, A108, CARD_2:63;
then consider z1 being
set such that A114:
A \ (A /\ B) = {z1}
by CARD_2:60;
consider z2 being
set such that A115:
B \ (A /\ B) = {z2}
by A113, CARD_2:60;
A116:
(
A = (A /\ B) \/ {z1} &
B = (A /\ B) \/ {z2} )
by A105, A114, A115, XBOOLE_1:45;
A117:
(
z1 in {z1} &
z2 in {z2} )
by TARSKI:def 1;
then A118:
(
z1 in A & not
z1 in A /\ B &
z2 in B & not
z2 in A /\ B )
by A114, A115, XBOOLE_0:def 5;
A119:
(
C <> A &
C <> B )
A121:
{A,B,C} is
clique
proof
let Z1,
Z2 be
POINT of
(G_ k,X);
:: according to COMBGRAS:def 2 :: thesis: ( Z1 in {A,B,C} & Z2 in {A,B,C} implies ex L being LINE of (G_ k,X) st {Z1,Z2} on L )
assume
(
Z1 in {A,B,C} &
Z2 in {A,B,C} )
;
:: thesis: ex L being LINE of (G_ k,X) st {Z1,Z2} on L
then
( (
Z1 = A or
Z1 = B or
Z1 = C ) & (
Z2 = A or
Z2 = B or
Z2 = C ) )
by ENUMSET1:def 1;
then
( (
Z1 c= A \/ B &
Z2 c= A \/ B ) or (
Z1 c= A \/ C &
Z2 c= A \/ C ) or (
Z1 c= B \/ C &
Z2 c= B \/ C ) )
by XBOOLE_1:11;
then
( (
Z1 on L &
Z2 on L ) or (
Z1 on L1 &
Z2 on L1 ) or (
Z1 on L2 &
Z2 on L2 ) )
by A4, A59, A110, A111, Th10;
then
(
{Z1,Z2} on L or
{Z1,Z2} on L1 or
{Z1,Z2} on L2 )
by INCSP_1:11;
hence
ex
L being
LINE of
(G_ k,X) st
{Z1,Z2} on L
;
:: thesis: verum
end;
A122:
3
c= card K
proof
assume
not 3
c= card K
;
:: thesis: contradiction
then
card K in 3
by ORDINAL1:26;
then
card K c= 2
by A8, ORDINAL1:34;
then A123:
card K = 2
by A43, XBOOLE_0:def 10;
then
(
K is
finite &
{A,B} is
finite &
A in {A,B,C} &
B in {A,B,C} & not
C in {A,B} &
C in {A,B,C} )
by A119, ENUMSET1:def 1, TARSKI:def 2;
then
(
K = {A,B} &
{A,B} c= {A,B,C} & not
{A,B,C} c= {A,B} )
by A44, A45, A48, A49, A123, CARD_FIN:1, ZFMISC_1:38;
hence
contradiction
by A9, A121, Def3;
:: thesis: verum
end;
card {A,B} <> card K
then
card {A,B} in card K
by A43, A44, A45, A48, A49, CARD_1:13;
then
K \ {A,B} <> {}
by CARD_2:4;
then consider E2 being
set such that A124:
E2 in K \ {A,B}
by XBOOLE_0:def 1;
A125:
(
E2 in K & not
E2 in {A,B} )
by A124, XBOOLE_0:def 5;
then A126:
(
E2 in the
Points of
(G_ k,X) &
E2 <> A &
E2 <> B )
by TARSKI:def 2;
then consider E1 being
Subset of
X such that A127:
(
E1 = E2 &
card E1 = k )
by A6;
consider E being
POINT of
(G_ k,X) such that A128:
E = E1
by A124, A127;
consider K1 being
LINE of
(G_ k,X) such that A129:
{A,E} on K1
by A10, A44, A46, A48, A125, A127, A128, Def2;
K1 in the
Lines of
(G_ k,X)
;
then consider M1 being
Subset of
X such that A130:
(
K1 = M1 &
card M1 = k + 1 )
by A7;
consider K2 being
LINE of
(G_ k,X) such that A131:
{B,E} on K2
by A10, A44, A46, A49, A125, A127, A128, Def2;
K2 in the
Lines of
(G_ k,X)
;
then consider M2 being
Subset of
X such that A132:
(
K2 = M2 &
card M2 = k + 1 )
by A7;
(
A on K1 &
E on K1 &
B on K2 &
E on K2 )
by A129, A131, INCSP_1:11;
then
(
A c= K1 &
E c= K1 &
B c= K2 &
E c= K2 )
by A4, Th10;
then
(
A \/ E c= K1 &
B \/ E c= K2 )
by XBOOLE_1:8;
then A133:
(
card (A \/ E) c= k + 1 &
card (B \/ E) c= k + 1 & not
E on L &
k + 1
c= card (A \/ E) &
k + 1
c= card (B \/ E) )
by A50, A51, A94, A125, A126, A127, A128, A130, A132, Th1, CARD_1:27;
then
(
card (A \/ E) = (k - 1) + (2 * 1) &
card (B \/ E) = (k - 1) + (2 * 1) &
card A = (k - 1) + 1 &
card B = (k - 1) + 1 &
card E = (k - 1) + 1 )
by A50, A51, A127, A128, XBOOLE_0:def 10;
then
(
card (A /\ E) = (k + 1) - 2 &
card (B /\ E) = (k + 1) - 2 &
card A = (k + 1) - 1 &
card B = (k + 1) - 1 &
card E = (k + 1) - 1 & 2
+ 1
<= k + 1 & 1
+ 1
<= k + 1 &
card (A /\ B) = (k + 1) - 2 )
by A1, A2, A5, A95, Th2, XREAL_1:9;
then A134:
( (
card ((A /\ B) /\ E) = (k + 1) - 2 &
card ((A \/ B) \/ E) = (k + 1) + 1 ) or (
card ((A /\ B) /\ E) = (k + 1) - 3 &
card ((A \/ B) \/ E) = k + 1 ) )
by Th7;
A135:
not
card ((A \/ B) \/ E) = k + 1
A /\ B = (A /\ B) /\ E
by A100, A108, A134, A135, CARD_FIN:1, XBOOLE_1:17;
then A138:
(
A /\ B c= E &
E is
finite )
by A127, A128, XBOOLE_1:17;
then
card (E \ (A /\ B)) = k - (k - 1)
by A108, A127, A128, CARD_2:63;
then consider z4 being
set such that A139:
E \ (A /\ B) = {z4}
by CARD_2:60;
A140:
E = (A /\ B) \/ {z4}
by A138, A139, XBOOLE_1:45;
A141:
K c= S
proof
assume
not
K c= S
;
:: thesis: contradiction
then consider D2 being
set such that A142:
(
D2 in K & not
D2 in S )
by TARSKI:def 3;
D2 in the
Points of
(G_ k,X)
by A142;
then consider D1 being
Subset of
X such that A143:
(
D1 = D2 &
card D1 = k )
by A6;
consider D being
POINT of
(G_ k,X) such that A144:
D = D1
by A142, A143;
not
A /\ B c= D
by A97, A142, A143, A144;
then consider y being
set such that A145:
(
y in A /\ B & not
y in D )
by TARSKI:def 3;
consider K11 being
LINE of
(G_ k,X) such that A146:
{A,D} on K11
by A10, A44, A46, A48, A142, A143, A144, Def2;
consider K12 being
LINE of
(G_ k,X) such that A147:
{B,D} on K12
by A10, A44, A46, A49, A142, A143, A144, Def2;
consider K13 being
LINE of
(G_ k,X) such that A148:
{E,D} on K13
by A10, A125, A127, A128, A142, A143, A144, Def2;
K11 in the
Lines of
(G_ k,X)
;
then consider R11 being
Subset of
X such that A149:
(
R11 = K11 &
card R11 = k + 1 )
by A7;
K12 in the
Lines of
(G_ k,X)
;
then consider R12 being
Subset of
X such that A150:
(
R12 = K12 &
card R12 = k + 1 )
by A7;
K13 in the
Lines of
(G_ k,X)
;
then consider R13 being
Subset of
X such that A151:
(
R13 = K13 &
card R13 = k + 1 )
by A7;
A152:
(
A <> D &
B <> D &
E <> D )
by A97, A105, A138, A142, A143, A144;
(
A on K11 &
D on K11 &
B on K12 &
D on K12 &
E on K13 &
D on K13 )
by A146, A147, A148, INCSP_1:11;
then
(
A c= K11 &
D c= K11 &
B c= K12 &
D c= K12 &
E c= K13 &
D c= K13 )
by A4, Th10;
then
(
A \/ D c= K11 &
B \/ D c= K12 &
E \/ D c= K13 )
by XBOOLE_1:8;
then
(
card (A \/ D) c= k + 1 &
card (B \/ D) c= k + 1 &
card (E \/ D) c= k + 1 &
k + 1
c= card (A \/ D) &
k + 1
c= card (B \/ D) &
k + 1
c= card (E \/ D) )
by A50, A51, A127, A128, A143, A144, A149, A150, A151, A152, Th1, CARD_1:27;
then
(
card (A \/ D) = (k - 1) + (2 * 1) &
card (B \/ D) = (k - 1) + (2 * 1) &
card (E \/ D) = (k - 1) + (2 * 1) &
card D = (k - 1) + 1 )
by A143, A144, XBOOLE_0:def 10;
then A153:
(
card (A /\ D) = k - 1 &
card (B /\ D) = k - 1 &
card (E /\ D) = k - 1 )
by A5, A50, A51, A127, A128, Th2;
( not
A /\ B c= (A /\ B) /\ D &
z4 in E \ (A /\ B) )
by A139, A145, TARSKI:def 1, XBOOLE_0:def 4;
then A154:
(
A /\ B <> (A /\ B) /\ D &
(A /\ B) /\ D c= A /\ B & not
z4 in A /\ B )
by XBOOLE_0:def 5, XBOOLE_1:17;
A155:
card ((A /\ B) /\ D) <> card (A /\ B)
by A112, A154, CARD_FIN:1;
A157:
(
z1 in D &
z2 in D &
z4 in D )
proof
assume
( not
z1 in D or not
z2 in D or not
z4 in D )
;
:: thesis: contradiction
then
( (
A /\ D = ((A /\ B) \/ {z1}) /\ D &
{z1} misses D ) or (
B /\ D = ((A /\ B) \/ {z2}) /\ D &
{z2} misses D ) or (
E /\ D = ((A /\ B) \/ {z4}) /\ D &
{z4} misses D ) )
by A105, A114, A115, A138, A139, XBOOLE_1:45, ZFMISC_1:56;
then
( (
A /\ D = ((A /\ B) /\ D) \/ ({z1} /\ D) &
{z1} /\ D = {} ) or (
B /\ D = ((A /\ B) /\ D) \/ ({z2} /\ D) &
{z2} /\ D = {} ) or (
E /\ D = ((A /\ B) /\ D) \/ ({z4} /\ D) &
{z4} /\ D = {} ) )
by XBOOLE_0:def 7, XBOOLE_1:23;
hence
contradiction
by A5, A107, A153, A155, Th2;
:: thesis: verum
end;
A158:
(A /\ B) /\ D is
finite
by A112;
then reconsider r =
card ((A /\ B) /\ D) as
Nat ;
A /\ D = ((A /\ B) \/ {z1}) /\ D
by A105, A114, XBOOLE_1:45;
then
(
A /\ D = ((A /\ B) /\ D) \/ ({z1} /\ D) &
{z1} /\ D = {z1} )
by A157, XBOOLE_1:23, ZFMISC_1:52;
then A161:
(
A /\ D = ((A /\ B) /\ D) \/ {z1} & not
z1 in (A /\ B) /\ D &
(A /\ B) /\ D c= D )
by A118, XBOOLE_0:def 4, XBOOLE_1:17;
then
card (A /\ D) = r + 1
by A158, CARD_2:54;
then A162:
card ((A /\ B) /\ D) = k - 2
by A153;
(
{z1,z2} c= D &
{z4} c= D )
by A157, ZFMISC_1:37, ZFMISC_1:38;
then
{z1,z2} \/ {z4} c= D
by XBOOLE_1:8;
then A163:
{z1,z2,z4} c= D
by ENUMSET1:43;
A164:
card {z1,z2,z4} = 3
by A45, A48, A49, A116, A126, A127, A128, A140, CARD_2:77;
{z1,z2,z4} misses (A /\ B) /\ D
proof
assume
not
{z1,z2,z4} misses (A /\ B) /\ D
;
:: thesis: contradiction
then
{z1,z2,z4} /\ ((A /\ B) /\ D) <> {}
by XBOOLE_0:def 7;
then consider m being
set such that A165:
m in {z1,z2,z4} /\ ((A /\ B) /\ D)
by XBOOLE_0:def 1;
A166:
(
m in {z1,z2,z4} &
m in (A /\ B) /\ D )
by A165, XBOOLE_0:def 4;
then
(
m = z1 or
m = z2 or
m = z4 )
by ENUMSET1:def 1;
hence
contradiction
by A114, A115, A117, A154, A166, XBOOLE_0:def 5;
:: thesis: verum
end;
then A167:
card (((A /\ B) /\ D) \/ {z1,z2,z4}) = (k - 2) + 3
by A158, A162, A164, CARD_2:53;
((A /\ B) /\ D) \/ {z1,z2,z4} c= D
by A161, A163, XBOOLE_1:8;
then
k + 1
c= k
by A143, A144, A167, CARD_1:27;
then
k in k
by A8, ORDINAL1:33;
hence
contradiction
;
:: thesis: verum
end;
S c= the
Points of
(G_ k,X)
then consider S1 being
Subset of the
Points of
(G_ k,X) such that A169:
S1 = S
;
A170:
S1 is
STAR
by A58, A97, A108, A169, Def4;
then
S1 is
maximal_clique
by A1, Th14;
then
S1 is
clique
by Def3;
hence
K is
STAR
by A9, A141, A169, A170, Def3;
:: thesis: verum
end;
hence
( K is STAR or K is TOP )
by A60; :: thesis: verum