A1:
succ 0 = 0 + 1
;
A2:
succ 2 = 2 + 1
;
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)) holds
( not K is maximal_clique or K is STAR or K is TOP )
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)) holds
( not K is maximal_clique or K is STAR or K is TOP ) )
assume that
A3:
2 <= k
and
A4:
k + 2 c= card X
; 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 )
k + 1 <= k + 2
by XREAL_1:7;
then A5:
k + 1 c= k + 2
by NAT_1:39;
then A6:
k + 1 c= card X
by A4, XBOOLE_1:1;
then A7:
the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k }
by A3, Def1;
A8:
succ (k + 1) = (k + 1) + 1
by NAT_1:38;
A9:
1 <= k
by A3, XXREAL_0:2;
let K be Subset of the Points of (G_ (k,X)); ( not K is maximal_clique or K is STAR or K is TOP )
A10:
succ k = k + 1
by NAT_1:38;
0 c= card K
;
then
0 in succ (card K)
by ORDINAL1:22;
then A11:
( card K = 0 or 0 in card K )
by ORDINAL1:8;
assume A12:
K is maximal_clique
; ( K is STAR or K is TOP )
then A13:
K is clique
by Def3;
A14:
the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 }
by A3, A6, Def1;
k <= k + 1
by NAT_1:11;
then A15:
k c= k + 1
by NAT_1:39;
then A16:
k c= card X
by A6, XBOOLE_1:1;
K <> {}
proof
consider A1 being
set such that A17:
A1 c= X
and A18:
card A1 = k
by A16, CARD_FIL:36;
A1 in the
Points of
(G_ (k,X))
by A7, A17, A18;
then consider A being
POINT of
(G_ (k,X)) such that A19:
A = A1
;
card A <> card X
then
card A in card X
by A16, A18, A19, CARD_1:3;
then
X \ A <> {}
by CARD_1:68;
then consider x being
set such that A20:
x in X \ A
by XBOOLE_0:def 1;
{x} c= X
by A20, ZFMISC_1:31;
then A21:
A \/ {x} c= X
by A17, A19, XBOOLE_1:8;
A22:
not
x in A
by A20, XBOOLE_0:def 5;
A is
finite
by A18, A19;
then
card (A \/ {x}) = k + 1
by A18, A19, A22, CARD_2:41;
then
A \/ {x} in the
Lines of
(G_ (k,X))
by A14, A21;
then consider L being
LINE of
(G_ (k,X)) such that A23:
L = A \/ {x}
;
consider U being
Subset of the
Points of
(G_ (k,X)) such that A24:
U = {A}
;
A c= L
by A23, XBOOLE_1:7;
then A25:
A on L
by A3, A6, Th10;
A26:
U is
clique
proof
let B,
C be
POINT of
(G_ (k,X));
COMBGRAS:def 2 ( 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 )
;
ex L being LINE of (G_ (k,X)) st {B,C} on L
then
(
B on L &
C on L )
by A25, A24, TARSKI:def 1;
then
{B,C} on L
by INCSP_1:1;
hence
ex
L being
LINE of
(G_ (k,X)) st
{B,C} on L
;
verum
end;
assume A27:
K = {}
;
contradiction
then
K c= U
by XBOOLE_1:2;
hence
contradiction
by A12, A27, A24, A26, Def3;
verum
end;
then
1 c= card K
by A1, A11, ORDINAL1:21;
then
1 in succ (card K)
by ORDINAL1:22;
then A28:
( card K = 1 or 1 in card K )
by ORDINAL1:8;
A29:
k - 1 is Element of NAT
by A3, NAT_1:21, XXREAL_0:2;
A30:
card K <> 1
proof
assume
card K = 1
;
contradiction
then consider A3 being
set such that A31:
K = {A3}
by CARD_2:42;
A32:
A3 in K
by A31, TARSKI:def 1;
then consider A being
POINT of
(G_ (k,X)) such that A33:
A = A3
;
A3 in the
Points of
(G_ (k,X))
by A32;
then A34:
ex
A4 being
Subset of
X st
(
A = A4 &
card A4 = k )
by A7, A33;
then A35:
A is
finite
;
A36:
card A <> card X
card A c= card X
by A6, A15, A34, XBOOLE_1:1;
then
card A in card X
by A36, CARD_1:3;
then
X \ A <> {}
by CARD_1:68;
then consider x being
set such that A37:
x in X \ A
by XBOOLE_0:def 1;
A38:
{x} c= X
by A37, ZFMISC_1:31;
then A39:
A \/ {x} c= X
by A34, XBOOLE_1:8;
not
x in A
by A37, XBOOLE_0:def 5;
then
card (A \/ {x}) = k + 1
by A34, A35, CARD_2:41;
then
A \/ {x} in the
Lines of
(G_ (k,X))
by A14, A39;
then consider L being
LINE of
(G_ (k,X)) such that A40:
L = A \/ {x}
;
k - 1
<= (k - 1) + 1
by A29, NAT_1:11;
then
k - 1
c= card A
by A29, A34, NAT_1:39;
then consider B2 being
set such that A41:
B2 c= A
and A42:
card B2 = k - 1
by A29, CARD_FIL:36;
A43:
B2 is
finite
by A3, A42, NAT_1:21, XXREAL_0:2;
B2 c= X
by A34, A41, XBOOLE_1:1;
then A44:
B2 \/ {x} c= X
by A38, XBOOLE_1:8;
not
x in B2
by A37, A41, XBOOLE_0:def 5;
then
card (B2 \/ {x}) = (k - 1) + 1
by A42, A43, CARD_2:41;
then
B2 \/ {x} in the
Points of
(G_ (k,X))
by A7, A44;
then consider A1 being
POINT of
(G_ (k,X)) such that A45:
A1 = B2 \/ {x}
;
A46:
{x} c= L
by A40, XBOOLE_1:7;
A47:
A c= L
by A40, XBOOLE_1:7;
then
B2 c= L
by A41, XBOOLE_1:1;
then
A1 c= L
by A45, A46, XBOOLE_1:8;
then A48:
A1 on L
by A3, A6, Th10;
{x} c= A1
by A45, XBOOLE_1:7;
then
x in A1
by ZFMISC_1:31;
then A49:
A <> A1
by A37, XBOOLE_0:def 5;
consider U being
Subset of the
Points of
(G_ (k,X)) such that A50:
U = {A,A1}
;
A51:
A on L
by A3, A6, A47, Th10;
A52:
U is
clique
proof
let B1,
B2 be
POINT of
(G_ (k,X));
COMBGRAS:def 2 ( 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 )
;
ex L being LINE of (G_ (k,X)) st {B1,B2} on L
then
(
B1 on L &
B2 on L )
by A51, A48, A50, TARSKI:def 2;
then
{B1,B2} on L
by INCSP_1:1;
hence
ex
L being
LINE of
(G_ (k,X)) st
{B1,B2} on L
;
verum
end;
A in U
by A50, TARSKI:def 2;
then A53:
K c= U
by A31, A33, ZFMISC_1:31;
A1 in U
by A50, TARSKI:def 2;
then
U <> K
by A31, A33, A49, TARSKI:def 1;
hence
contradiction
by A12, A53, A52, Def3;
verum
end;
succ 1 = 1 + 1
;
then A54:
2 c= card K
by A30, A28, ORDINAL1:21;
then consider R being set such that
A55:
R c= K
and
A56:
card R = 2
by CARD_FIL:36;
R is finite
by A56;
then consider A1, B1 being set such that
A57:
A1 <> B1
and
A58:
R = {A1,B1}
by A56, CARD_2:60;
A59:
A1 in R
by A58, TARSKI:def 2;
then A60:
A1 in the Points of (G_ (k,X))
by A55, TARSKI:def 3;
then consider A being POINT of (G_ (k,X)) such that
A61:
A = A1
;
A62:
B1 in R
by A58, TARSKI:def 2;
then A63:
B1 in the Points of (G_ (k,X))
by A55, TARSKI:def 3;
then consider B being POINT of (G_ (k,X)) such that
A64:
B = B1
;
consider L being LINE of (G_ (k,X)) such that
A65:
{A,B} on L
by A13, A55, A59, A62, A61, A64, Def2;
L in the Lines of (G_ (k,X))
;
then A66:
ex L1 being Subset of X st
( L1 = L & card L1 = k + 1 )
by A14;
then A67:
L is finite
;
A on L
by A65, INCSP_1:1;
then A68:
A c= L
by A3, A6, Th10;
then A69:
A /\ B c= L
by XBOOLE_1:108;
then A70:
A /\ B c= X
by A66, XBOOLE_1:1;
B on L
by A65, INCSP_1:1;
then A71:
B c= L
by A3, A6, Th10;
then A72:
A \/ B c= L
by A68, XBOOLE_1:8;
then A73:
card (A \/ B) c= k + 1
by A66, CARD_1:11;
A74:
ex B2 being Subset of X st
( B2 = B & card B2 = k )
by A7, A63, A64;
then A75:
B is finite
;
A76:
ex A2 being Subset of X st
( A2 = A & card A2 = k )
by A7, A60, A61;
then A77:
A is finite
;
A78:
k + 1 c= card (A \/ B)
by A57, A61, A64, A76, A74, Th1;
then A79:
card (A \/ B) = k + 1
by A73, XBOOLE_0:def 10;
then A80:
A \/ B = L
by A68, A71, A66, A67, CARD_FIN:1, XBOOLE_1:8;
A81:
( ( 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
A82:
card L <> card X
card L c= card X
by A4, A5, A66, XBOOLE_1:1;
then
card L in card X
by A82, CARD_1:3;
then
X \ L <> {}
by CARD_1:68;
then consider x being
set such that A83:
x in X \ L
by XBOOLE_0:def 1;
A84:
( not
x in A & not
x in B )
by A68, A71, A83, XBOOLE_0:def 5;
A85:
(
A /\ {x} = {} &
B /\ {x} = {} )
A87:
(
card A = (k - 1) + 1 &
card (A \/ B) = (k - 1) + (2 * 1) )
by A76, A73, A78, XBOOLE_0:def 10;
then A88:
card (A /\ B) = k - 1
by A29, A74, Th2;
then
card (A \ (A /\ B)) = k - (k - 1)
by A76, A77, CARD_2:44, XBOOLE_1:17;
then consider z1 being
set such that A89:
A \ (A /\ B) = {z1}
by CARD_2:42;
card (B \ (A /\ B)) = k - (k - 1)
by A74, A75, A88, CARD_2:44, XBOOLE_1:17;
then consider z2 being
set such that A90:
B \ (A /\ B) = {z2}
by CARD_2:42;
A91:
B = (A /\ B) \/ {z2}
by A90, XBOOLE_1:17, XBOOLE_1:45;
A92:
z2 in {z2}
by TARSKI:def 1;
A93:
card (A \/ B) = (k - 1) + (2 * 1)
by A73, A78, XBOOLE_0:def 10;
A94:
not
x in A /\ B
by A69, A83, XBOOLE_0:def 5;
card A = (k - 1) + 1
by A76;
then
card (A /\ B) = k - 1
by A29, A74, A93, Th2;
then A95:
card ((A /\ B) \/ {x}) = (k - 1) + 1
by A68, A67, A94, CARD_2:41;
{x} c= X
by A83, ZFMISC_1:31;
then A96:
(A /\ B) \/ {x} c= X
by A70, XBOOLE_1:8;
then
(A /\ B) \/ {x} in the
Points of
(G_ (k,X))
by A7, A95;
then consider C being
POINT of
(G_ (k,X)) such that A97:
C = (A /\ B) \/ {x}
;
A98:
B \/ C c= X
by A74, A96, A97, XBOOLE_1:8;
A99:
A \/ C c= X
by A76, A96, A97, XBOOLE_1:8;
A100:
1
+ 1
<= k + 1
by A9, XREAL_1:7;
A101:
A /\ B c= B
by XBOOLE_1:17;
B /\ C = (B /\ {x}) \/ (B /\ (B /\ A))
by A97, XBOOLE_1:23;
then
B /\ C = (B /\ {x}) \/ ((B /\ B) /\ A)
by XBOOLE_1:16;
then
card (B /\ C) = k - 1
by A29, A74, A85, A87, Th2;
then
card (B \/ C) = (k - 1) + (2 * 1)
by A29, A74, A95, A97, Th2;
then
B \/ C in the
Lines of
(G_ (k,X))
by A14, A98;
then consider L2 being
LINE of
(G_ (k,X)) such that A102:
L2 = B \/ C
;
A /\ C = (A /\ {x}) \/ (A /\ (A /\ B))
by A97, XBOOLE_1:23;
then
A /\ C = (A /\ {x}) \/ ((A /\ A) /\ B)
by XBOOLE_1:16;
then
card (A /\ C) = k - 1
by A29, A74, A85, A87, Th2;
then
card (A \/ C) = (k - 1) + (2 * 1)
by A29, A76, A95, A97, Th2;
then
A \/ C in the
Lines of
(G_ (k,X))
by A14, A99;
then consider L1 being
LINE of
(G_ (k,X)) such that A103:
L1 = A \/ C
;
A104:
{A,B,C} is
clique
proof
let Z1,
Z2 be
POINT of
(G_ (k,X));
COMBGRAS:def 2 ( 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 that A105:
Z1 in {A,B,C}
and A106:
Z2 in {A,B,C}
;
ex L being LINE of (G_ (k,X)) st {Z1,Z2} on L
A107:
(
Z2 = A or
Z2 = B or
Z2 = C )
by A106, ENUMSET1:def 1;
(
Z1 = A or
Z1 = B or
Z1 = C )
by A105, 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 A107, 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 A3, A6, A80, A103, A102, Th10;
then
(
{Z1,Z2} on L or
{Z1,Z2} on L1 or
{Z1,Z2} on L2 )
by INCSP_1:1;
hence
ex
L being
LINE of
(G_ (k,X)) st
{Z1,Z2} on L
;
verum
end;
A108:
(
C <> A &
C <> B )
A110:
3
c= card K
proof
assume
not 3
c= card K
;
contradiction
then
card K in 3
by ORDINAL1:16;
then
card K c= 2
by A2, ORDINAL1:22;
then
(
card K = 2 &
K is
finite )
by A54, XBOOLE_0:def 10;
then A111:
K = {A,B}
by A55, A56, A58, A61, A64, CARD_FIN:1;
(
A in {A,B,C} &
B in {A,B,C} )
by ENUMSET1:def 1;
then A112:
{A,B} c= {A,B,C}
by ZFMISC_1:32;
C in {A,B,C}
by ENUMSET1:def 1;
then
not
{A,B,C} c= {A,B}
by A108, TARSKI:def 2;
hence
contradiction
by A12, A104, A111, A112, Def3;
verum
end;
card {A,B} <> card K
then
card {A,B} in card K
by A54, A56, A58, A61, A64, CARD_1:3;
then
K \ {A,B} <> {}
by CARD_1:68;
then consider E2 being
set such that A113:
E2 in K \ {A,B}
by XBOOLE_0:def 1;
A114:
card A = (k - 1) + 1
by A76;
then A115:
card (A /\ B) = (k + 1) - 2
by A29, A74, A93, Th2;
A116:
card B = (k - 1) + 1
by A74;
A117:
A /\ B c= A
by XBOOLE_1:17;
A118:
not
E2 in {A,B}
by A113, XBOOLE_0:def 5;
then A119:
E2 <> A
by TARSKI:def 2;
E2 in the
Points of
(G_ (k,X))
by A113;
then consider E1 being
Subset of
X such that A120:
E1 = E2
and A121:
card E1 = k
by A7;
consider E being
POINT of
(G_ (k,X)) such that A122:
E = E1
by A113, A120;
A123:
A = (A /\ B) \/ {z1}
by A89, XBOOLE_1:17, XBOOLE_1:45;
A124:
z1 in {z1}
by TARSKI:def 1;
then A125:
not
z1 in A /\ B
by A89, XBOOLE_0:def 5;
A126:
(
card A = (k + 1) - 1 & 2
+ 1
<= k + 1 )
by A3, A76, XREAL_1:7;
consider S being
set such that A127:
S = { D where D is Subset of X : ( card D = k & A /\ B c= D ) }
;
A128:
E2 in K
by A113, XBOOLE_0:def 5;
then consider K1 being
LINE of
(G_ (k,X)) such that A129:
{A,E} on K1
by A13, A55, A59, A61, A120, A122, Def2;
consider K2 being
LINE of
(G_ (k,X)) such that A130:
{B,E} on K2
by A13, A55, A62, A64, A128, A120, A122, Def2;
E on K2
by A130, INCSP_1:1;
then A131:
E c= K2
by A3, A6, Th10;
K2 in the
Lines of
(G_ (k,X))
;
then A132:
ex
M2 being
Subset of
X st
(
K2 = M2 &
card M2 = k + 1 )
by A14;
B on K2
by A130, INCSP_1:1;
then
B c= K2
by A3, A6, Th10;
then
B \/ E c= K2
by A131, XBOOLE_1:8;
then A133:
card (B \/ E) c= k + 1
by A132, CARD_1:11;
A134:
E2 <> B
by A118, TARSKI:def 2;
then
k + 1
c= card (B \/ E)
by A74, A120, A121, A122, Th1;
then
card (B \/ E) = (k - 1) + (2 * 1)
by A133, XBOOLE_0:def 10;
then A135:
card (B /\ E) = (k + 1) - 2
by A29, A121, A122, A116, Th2;
assume
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 )
;
K is STAR
then A136:
not
E on L
by A128, A119, A134, A120, A122;
A137:
not
card ((A \/ B) \/ E) = k + 1
E on K1
by A129, INCSP_1:1;
then A140:
E c= K1
by A3, A6, Th10;
K1 in the
Lines of
(G_ (k,X))
;
then A141:
ex
M1 being
Subset of
X st
(
K1 = M1 &
card M1 = k + 1 )
by A14;
A on K1
by A129, INCSP_1:1;
then
A c= K1
by A3, A6, Th10;
then
A \/ E c= K1
by A140, XBOOLE_1:8;
then A142:
card (A \/ E) c= k + 1
by A141, CARD_1:11;
k + 1
c= card (A \/ E)
by A76, A119, A120, A121, A122, Th1;
then
card (A \/ E) = (k - 1) + (2 * 1)
by A142, XBOOLE_0:def 10;
then
card (A /\ E) = (k + 1) - 2
by A29, A121, A122, A114, Th2;
then
( (
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 A74, A121, A122, A135, A126, A100, A115, Th7;
then A143:
A /\ B = (A /\ B) /\ E
by A68, A67, A88, A137, CARD_FIN:1, XBOOLE_1:17;
then A144:
A /\ B c= E
by XBOOLE_1:17;
E is
finite
by A121, A122;
then
card (E \ (A /\ B)) = k - (k - 1)
by A88, A121, A122, A143, CARD_2:44, XBOOLE_1:17;
then consider z4 being
set such that A145:
E \ (A /\ B) = {z4}
by CARD_2:42;
A146:
E = (A /\ B) \/ {z4}
by A143, A145, XBOOLE_1:17, XBOOLE_1:45;
A147:
K c= S
proof
assume
not
K c= S
;
contradiction
then consider D2 being
set such that A148:
D2 in K
and A149:
not
D2 in S
by TARSKI:def 3;
D2 in the
Points of
(G_ (k,X))
by A148;
then consider D1 being
Subset of
X such that A150:
D1 = D2
and A151:
card D1 = k
by A7;
consider D being
POINT of
(G_ (k,X)) such that A152:
D = D1
by A148, A150;
consider K11 being
LINE of
(G_ (k,X)) such that A153:
{A,D} on K11
by A13, A55, A59, A61, A148, A150, A152, Def2;
D on K11
by A153, INCSP_1:1;
then A154:
D c= K11
by A3, A6, Th10;
K11 in the
Lines of
(G_ (k,X))
;
then A155:
ex
R11 being
Subset of
X st
(
R11 = K11 &
card R11 = k + 1 )
by A14;
A156:
card D = (k - 1) + 1
by A151, A152;
consider K13 being
LINE of
(G_ (k,X)) such that A157:
{E,D} on K13
by A13, A128, A120, A122, A148, A150, A152, Def2;
consider K12 being
LINE of
(G_ (k,X)) such that A158:
{B,D} on K12
by A13, A55, A62, A64, A148, A150, A152, Def2;
A on K11
by A153, INCSP_1:1;
then
A c= K11
by A3, A6, Th10;
then
A \/ D c= K11
by A154, XBOOLE_1:8;
then A159:
card (A \/ D) c= k + 1
by A155, CARD_1:11;
A <> D
by A127, A117, A149, A150, A151, A152;
then
k + 1
c= card (A \/ D)
by A76, A151, A152, Th1;
then
card (A \/ D) = (k - 1) + (2 * 1)
by A159, XBOOLE_0:def 10;
then A160:
card (A /\ D) = k - 1
by A29, A76, A156, Th2;
not
A /\ B c= D
by A127, A149, A150, A151, A152;
then
ex
y being
set st
(
y in A /\ B & not
y in D )
by TARSKI:def 3;
then
A /\ B <> (A /\ B) /\ D
by XBOOLE_0:def 4;
then A161:
card ((A /\ B) /\ D) <> card (A /\ B)
by A77, CARD_FIN:1, XBOOLE_1:17;
D on K13
by A157, INCSP_1:1;
then A162:
D c= K13
by A3, A6, Th10;
K13 in the
Lines of
(G_ (k,X))
;
then A163:
ex
R13 being
Subset of
X st
(
R13 = K13 &
card R13 = k + 1 )
by A14;
D on K12
by A158, INCSP_1:1;
then A164:
D c= K12
by A3, A6, Th10;
K12 in the
Lines of
(G_ (k,X))
;
then A165:
ex
R12 being
Subset of
X st
(
R12 = K12 &
card R12 = k + 1 )
by A14;
B on K12
by A158, INCSP_1:1;
then
B c= K12
by A3, A6, Th10;
then
B \/ D c= K12
by A164, XBOOLE_1:8;
then A166:
card (B \/ D) c= k + 1
by A165, CARD_1:11;
B <> D
by A127, A101, A149, A150, A151, A152;
then
k + 1
c= card (B \/ D)
by A74, A151, A152, Th1;
then
card (B \/ D) = (k - 1) + (2 * 1)
by A166, XBOOLE_0:def 10;
then A167:
card (B /\ D) = k - 1
by A29, A74, A156, Th2;
E on K13
by A157, INCSP_1:1;
then
E c= K13
by A3, A6, Th10;
then
E \/ D c= K13
by A162, XBOOLE_1:8;
then A168:
card (E \/ D) c= k + 1
by A163, CARD_1:11;
E <> D
by A127, A144, A149, A150, A151, A152;
then
k + 1
c= card (E \/ D)
by A121, A122, A151, A152, Th1;
then
card (E \/ D) = (k - 1) + (2 * 1)
by A168, XBOOLE_0:def 10;
then A169:
card (E /\ D) = k - 1
by A29, A121, A122, A156, Th2;
A170:
(
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 )
;
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 A89, A90, A143, A145, XBOOLE_1:17, XBOOLE_1:45, ZFMISC_1:50;
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 A29, A74, A87, A160, A167, A169, A161, Th2;
verum
end;
then
(
{z1,z2} c= D &
{z4} c= D )
by ZFMISC_1:31, ZFMISC_1:32;
then
{z1,z2} \/ {z4} c= D
by XBOOLE_1:8;
then
(
(A /\ B) /\ D c= D &
{z1,z2,z4} c= D )
by ENUMSET1:3, XBOOLE_1:17;
then A171:
((A /\ B) /\ D) \/ {z1,z2,z4} c= D
by XBOOLE_1:8;
A172:
(
z4 in E \ (A /\ B) &
(A /\ B) /\ D c= A /\ B )
by A145, TARSKI:def 1, XBOOLE_1:17;
A173:
{z1,z2,z4} misses (A /\ B) /\ D
proof
assume
not
{z1,z2,z4} misses (A /\ B) /\ D
;
contradiction
then
{z1,z2,z4} /\ ((A /\ B) /\ D) <> {}
by XBOOLE_0:def 7;
then consider m being
set such that A174:
m in {z1,z2,z4} /\ ((A /\ B) /\ D)
by XBOOLE_0:def 1;
m in {z1,z2,z4}
by A174, XBOOLE_0:def 4;
then A175:
(
m = z1 or
m = z2 or
m = z4 )
by ENUMSET1:def 1;
m in (A /\ B) /\ D
by A174, XBOOLE_0:def 4;
hence
contradiction
by A89, A90, A124, A92, A172, A175, XBOOLE_0:def 5;
verum
end;
reconsider r =
card ((A /\ B) /\ D) as
Nat by A77;
A176:
not
z1 in (A /\ B) /\ D
by A125, XBOOLE_0:def 4;
A /\ D = ((A /\ B) \/ {z1}) /\ D
by A89, XBOOLE_1:17, XBOOLE_1:45;
then
A /\ D = ((A /\ B) /\ D) \/ ({z1} /\ D)
by XBOOLE_1:23;
then
A /\ D = ((A /\ B) /\ D) \/ {z1}
by A170, ZFMISC_1:46;
then A177:
card (A /\ D) = r + 1
by A77, A176, CARD_2:41;
card {z1,z2,z4} = 3
by A57, A61, A64, A123, A91, A119, A134, A120, A122, A146, CARD_2:58;
then
card (((A /\ B) /\ D) \/ {z1,z2,z4}) = (k - 2) + 3
by A77, A160, A177, A173, CARD_2:40;
then
k + 1
c= k
by A151, A152, A171, CARD_1:11;
then
k in k
by A10, ORDINAL1:21;
hence
contradiction
;
verum
end;
S c= the
Points of
(G_ (k,X))
then consider S1 being
Subset of the
Points of
(G_ (k,X)) such that A178:
S1 = S
;
A179:
S1 is
STAR
by A70, A127, A88, A178, Def4;
then
S1 is
maximal_clique
by A3, A4, Th14;
then
S1 is
clique
by Def3;
hence
K is
STAR
by A12, A147, A178, A179, Def3;
verum
end;
A180:
k - 2 is Element of NAT
by A3, NAT_1:21;
then A181:
succ (k - 2) = (k - 2) + 1
by NAT_1:38;
( ex C being POINT of (G_ (k,X)) st
( C in K & C on L & A <> C & B <> C ) implies K is TOP )
proof
A182:
1
+ 1
<= k + 1
by A9, XREAL_1:7;
A183:
card B = (k - 1) + 1
by A74;
A184:
card A = (k - 1) + 1
by A76;
assume
ex
C being
POINT of
(G_ (k,X)) st
(
C in K &
C on L &
A <> C &
B <> C )
;
K is TOP
then consider C being
POINT of
(G_ (k,X)) such that A185:
C in K
and A186:
C on L
and A187:
A <> C
and A188:
B <> C
;
A189:
C c= L
by A3, A6, A186, Th10;
then
A \/ C c= L
by A68, XBOOLE_1:8;
then A190:
card (A \/ C) c= k + 1
by A66, CARD_1:11;
B \/ C c= L
by A71, A189, XBOOLE_1:8;
then A191:
card (B \/ C) c= k + 1
by A66, CARD_1:11;
C in the
Points of
(G_ (k,X))
;
then A192:
ex
C2 being
Subset of
X st
(
C2 = C &
card C2 = k )
by A7;
then
k + 1
c= card (B \/ C)
by A74, A188, Th1;
then
card (B \/ C) = (k - 1) + (2 * 1)
by A191, XBOOLE_0:def 10;
then A193:
card (B /\ C) = (k + 1) - 2
by A29, A192, A183, Th2;
k + 1
c= card (A \/ C)
by A76, A187, A192, Th1;
then
card (A \/ C) = (k - 1) + (2 * 1)
by A190, XBOOLE_0:def 10;
then A194:
card (A /\ C) = (k + 1) - 2
by A29, A192, A184, Th2;
A195:
card (A \/ B) = (k - 1) + (2 * 1)
by A73, A78, XBOOLE_0:def 10;
then A196:
A \/ B = L
by A68, A71, A66, A67, CARD_FIN:1, XBOOLE_1:8;
A197:
A \/ B c= (A \/ B) \/ C
by XBOOLE_1:7;
(A \/ B) \/ C c= L
by A72, A189, XBOOLE_1:8;
then A198:
card ((A \/ B) \/ C) = k + 1
by A195, A196, A197, XBOOLE_0:def 10;
A199:
(
card A = (k + 1) - 1 & 2
+ 1
<= k + 1 )
by A3, A76, XREAL_1:7;
consider T being
set such that A200:
T = { D where D is Subset of X : ( card D = k & D c= L ) }
;
card (A /\ B) = k - 1
by A29, A74, A195, A184, Th2;
then A201:
( (
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 A74, A192, A194, A199, A193, A182, Th7;
A202:
K c= T
proof
let D2 be
set ;
TARSKI:def 3 ( not D2 in K or D2 in T )
assume that A203:
D2 in K
and A204:
not
D2 in T
;
contradiction
D2 in the
Points of
(G_ (k,X))
by A203;
then consider D1 being
Subset of
X such that A205:
D1 = D2
and A206:
card D1 = k
by A7;
consider D being
POINT of
(G_ (k,X)) such that A207:
D = D1
by A203, A205;
not
D c= L
by A200, A204, A205, A206, A207;
then consider x being
set such that A208:
x in D
and A209:
not
x in L
by TARSKI:def 3;
A210:
card {x} = 1
by CARD_1:30;
A211:
D is
finite
by A206, A207;
A212:
card D = (k - 1) + 1
by A206, A207;
{x} c= D
by A208, ZFMISC_1:31;
then A213:
card (D \ {x}) = k - 1
by A206, A207, A211, A210, CARD_2:44;
consider L13 being
LINE of
(G_ (k,X)) such that A214:
{C,D} on L13
by A13, A185, A203, A205, A207, Def2;
D on L13
by A214, INCSP_1:1;
then A215:
D c= L13
by A3, A6, Th10;
L13 in the
Lines of
(G_ (k,X))
;
then A216:
ex
L23 being
Subset of
X st
(
L23 = L13 &
card L23 = k + 1 )
by A14;
C on L13
by A214, INCSP_1:1;
then
C c= L13
by A3, A6, Th10;
then
C \/ D c= L13
by A215, XBOOLE_1:8;
then A217:
card (C \/ D) c= k + 1
by A216, CARD_1:11;
A218:
not
x in C
by A189, A209;
A219:
C /\ D c= D \ {x}
C <> D
by A189, A200, A204, A205, A206, A207;
then
k + 1
c= card (C \/ D)
by A192, A206, A207, Th1;
then
card (C \/ D) = (k - 1) + (2 * 1)
by A217, XBOOLE_0:def 10;
then
card (C /\ D) = k - 1
by A29, A192, A212, Th2;
then A222:
C /\ D = D \ {x}
by A211, A213, A219, CARD_FIN:1;
consider L12 being
LINE of
(G_ (k,X)) such that A223:
{B,D} on L12
by A13, A55, A62, A64, A203, A205, A207, Def2;
consider L11 being
LINE of
(G_ (k,X)) such that A224:
{A,D} on L11
by A13, A55, A59, A61, A203, A205, A207, Def2;
D on L11
by A224, INCSP_1:1;
then A225:
D c= L11
by A3, A6, Th10;
L11 in the
Lines of
(G_ (k,X))
;
then A226:
ex
L21 being
Subset of
X st
(
L21 = L11 &
card L21 = k + 1 )
by A14;
A on L11
by A224, INCSP_1:1;
then
A c= L11
by A3, A6, Th10;
then
A \/ D c= L11
by A225, XBOOLE_1:8;
then A227:
card (A \/ D) c= k + 1
by A226, CARD_1:11;
A228:
not
x in A
by A68, A209;
A229:
A /\ D c= D \ {x}
A <> D
by A68, A200, A204, A205, A206, A207;
then
k + 1
c= card (A \/ D)
by A76, A206, A207, Th1;
then A232:
card (A \/ D) = (k - 1) + (2 * 1)
by A227, XBOOLE_0:def 10;
then
card (A /\ D) = k - 1
by A29, A76, A212, Th2;
then A233:
A /\ D = D \ {x}
by A211, A213, A229, CARD_FIN:1;
D on L12
by A223, INCSP_1:1;
then A234:
D c= L12
by A3, A6, Th10;
L12 in the
Lines of
(G_ (k,X))
;
then A235:
ex
L22 being
Subset of
X st
(
L22 = L12 &
card L22 = k + 1 )
by A14;
B on L12
by A223, INCSP_1:1;
then
B c= L12
by A3, A6, Th10;
then
B \/ D c= L12
by A234, XBOOLE_1:8;
then A236:
card (B \/ D) c= k + 1
by A235, CARD_1:11;
A237:
not
x in B
by A71, A209;
A238:
B /\ D c= D \ {x}
B <> D
by A71, A200, A204, A205, A206, A207;
then
k + 1
c= card (B \/ D)
by A74, A206, A207, Th1;
then
card (B \/ D) = (k - 1) + (2 * 1)
by A236, XBOOLE_0:def 10;
then
card (B /\ D) = k - 1
by A29, A74, A212, Th2;
then
B /\ D = D \ {x}
by A211, A213, A238, CARD_FIN:1;
then
A /\ D = (A /\ D) /\ (B /\ D)
by A233;
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 A233, A222;
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
by A29, A76, A212, A232, Th2;
then
k - 1
c= k - 2
by A198, A201, CARD_1:11, XBOOLE_1:17;
then
k - 1
in k - 1
by A180, A181, ORDINAL1:22;
hence
contradiction
;
verum
end;
T c= the
Points of
(G_ (k,X))
then consider T1 being
Subset of the
Points of
(G_ (k,X)) such that A241:
T1 = T
;
A242:
T1 is
TOP
by A66, A200, A241, Def5;
then
T1 is
maximal_clique
by A3, A4, Th14;
then
T1 is
clique
by Def3;
hence
K is
TOP
by A12, A202, A241, A242, Def3;
verum
end;
hence
( K is STAR or K is TOP )
by A81; verum