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:
Segm (k + 1) c= Segm (k + 2)
by NAT_1:39;
then A6:
k + 1 c= card X
by A4;
then A7:
the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k }
by A3, Def1;
A8:
succ (Segm (k + 1)) = Segm ((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 (Segm k) = Segm (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
;
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:
Segm k c= Segm (k + 1)
by NAT_1:39;
then A16:
k c= card X
by A6;
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
object 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
;
hence
contradiction
by A12, A27, A24, A26;
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;
then reconsider k1 = k - 1 as Nat ;
A30:
card K <> 1
proof
assume
card K = 1
;
contradiction
then consider A3 being
object 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 reconsider AA =
A as
finite set ;
A35:
A is
finite
by A34;
A36:
card A <> card X
card A c= card X
by A6, A15, A34;
then
card A in card X
by A36, CARD_1:3;
then
X \ A <> {}
by CARD_1:68;
then consider x being
object 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
Segm k1 c= Segm (card AA)
by A34, NAT_1:39;
then consider B2 being
set such that A41:
B2 c= A
and A42:
card B2 = k - 1
by 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;
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;
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;
consider A1, B1 being object 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;
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_2:102, 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;
then
card L in card X
by A82, CARD_1:3;
then
X \ L <> {}
by CARD_1:68;
then consider x being
object 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
object 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
object 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 )
by A84, A97, XBOOLE_1:11, ZFMISC_1:31;
A109:
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 A110:
K = {A,B}
by A55, A56, A58, A61, A64, CARD_2:102;
(
A in {A,B,C} &
B in {A,B,C} )
by ENUMSET1:def 1;
then A111:
{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, A110, A111;
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
object such that A112:
E2 in K \ {A,B}
by XBOOLE_0:def 1;
A113:
card A = (k - 1) + 1
by A76;
then A114:
card (A /\ B) = (k + 1) - 2
by A29, A74, A93, Th2;
A115:
card B = (k - 1) + 1
by A74;
A116:
A /\ B c= A
by XBOOLE_1:17;
A117:
not
E2 in {A,B}
by A112, XBOOLE_0:def 5;
then A118:
E2 <> A
by TARSKI:def 2;
E2 in the
Points of
(G_ (k,X))
by A112;
then consider E1 being
Subset of
X such that A119:
E1 = E2
and A120:
card E1 = k
by A7;
consider E being
POINT of
(G_ (k,X)) such that A121:
E = E1
by A112, A119;
A122:
A = (A /\ B) \/ {z1}
by A89, XBOOLE_1:17, XBOOLE_1:45;
A123:
z1 in {z1}
by TARSKI:def 1;
then A124:
not
z1 in A /\ B
by A89, XBOOLE_0:def 5;
A125:
(
card A = (k + 1) - 1 & 2
+ 1
<= k + 1 )
by A3, A76, XREAL_1:7;
consider S being
set such that A126:
S = { D where D is Subset of X : ( card D = k & A /\ B c= D ) }
;
A127:
E2 in K
by A112, XBOOLE_0:def 5;
then consider K1 being
LINE of
(G_ (k,X)) such that A128:
{A,E} on K1
by A13, A55, A59, A61, A119, A121;
consider K2 being
LINE of
(G_ (k,X)) such that A129:
{B,E} on K2
by A13, A55, A62, A64, A127, A119, A121;
E on K2
by A129, INCSP_1:1;
then A130:
E c= K2
by A3, A6, Th10;
K2 in the
Lines of
(G_ (k,X))
;
then A131:
ex
M2 being
Subset of
X st
(
K2 = M2 &
card M2 = k + 1 )
by A14;
B on K2
by A129, INCSP_1:1;
then
B c= K2
by A3, A6, Th10;
then
B \/ E c= K2
by A130, XBOOLE_1:8;
then A132:
card (B \/ E) c= k + 1
by A131, CARD_1:11;
A133:
E2 <> B
by A117, TARSKI:def 2;
then
k + 1
c= card (B \/ E)
by A74, A119, A120, A121, Th1;
then
card (B \/ E) = (k - 1) + (2 * 1)
by A132, XBOOLE_0:def 10;
then A134:
card (B /\ E) = (k + 1) - 2
by A29, A120, A121, A115, 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 A135:
not
E on L
by A127, A118, A133, A119, A121;
A136:
not
card ((A \/ B) \/ E) = k + 1
E on K1
by A128, INCSP_1:1;
then A139:
E c= K1
by A3, A6, Th10;
K1 in the
Lines of
(G_ (k,X))
;
then A140:
ex
M1 being
Subset of
X st
(
K1 = M1 &
card M1 = k + 1 )
by A14;
A on K1
by A128, INCSP_1:1;
then
A c= K1
by A3, A6, Th10;
then
A \/ E c= K1
by A139, XBOOLE_1:8;
then A141:
card (A \/ E) c= k + 1
by A140, CARD_1:11;
k + 1
c= card (A \/ E)
by A76, A118, A119, A120, A121, Th1;
then
card (A \/ E) = (k - 1) + (2 * 1)
by A141, XBOOLE_0:def 10;
then
card (A /\ E) = (k + 1) - 2
by A29, A120, A121, A113, 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, A120, A121, A134, A125, A100, A114, Th7;
then A142:
A /\ B = (A /\ B) /\ E
by A68, A67, A88, A136, CARD_2:102, XBOOLE_1:17;
then A143:
A /\ B c= E
by XBOOLE_1:17;
E is
finite
by A120, A121;
then
card (E \ (A /\ B)) = k - (k - 1)
by A88, A120, A121, A142, CARD_2:44, XBOOLE_1:17;
then consider z4 being
object such that A144:
E \ (A /\ B) = {z4}
by CARD_2:42;
A145:
E = (A /\ B) \/ {z4}
by A142, A144, XBOOLE_1:17, XBOOLE_1:45;
A146:
K c= S
proof
assume
not
K c= S
;
contradiction
then consider D2 being
object such that A147:
D2 in K
and A148:
not
D2 in S
;
D2 in the
Points of
(G_ (k,X))
by A147;
then consider D1 being
Subset of
X such that A149:
D1 = D2
and A150:
card D1 = k
by A7;
consider D being
POINT of
(G_ (k,X)) such that A151:
D = D1
by A147, A149;
consider K11 being
LINE of
(G_ (k,X)) such that A152:
{A,D} on K11
by A13, A55, A59, A61, A147, A149, A151;
D on K11
by A152, INCSP_1:1;
then A153:
D c= K11
by A3, A6, Th10;
K11 in the
Lines of
(G_ (k,X))
;
then A154:
ex
R11 being
Subset of
X st
(
R11 = K11 &
card R11 = k + 1 )
by A14;
A155:
card D = (k - 1) + 1
by A150, A151;
consider K13 being
LINE of
(G_ (k,X)) such that A156:
{E,D} on K13
by A13, A127, A119, A121, A147, A149, A151;
consider K12 being
LINE of
(G_ (k,X)) such that A157:
{B,D} on K12
by A13, A55, A62, A64, A147, A149, A151;
A on K11
by A152, INCSP_1:1;
then
A c= K11
by A3, A6, Th10;
then
A \/ D c= K11
by A153, XBOOLE_1:8;
then A158:
card (A \/ D) c= k + 1
by A154, CARD_1:11;
A <> D
by A126, A116, A148, A149, A150, A151;
then
k + 1
c= card (A \/ D)
by A76, A150, A151, Th1;
then
card (A \/ D) = (k - 1) + (2 * 1)
by A158, XBOOLE_0:def 10;
then A159:
card (A /\ D) = k - 1
by A29, A76, A155, Th2;
not
A /\ B c= D
by A126, A148, A149, A150, A151;
then
ex
y being
object st
(
y in A /\ B & not
y in D )
;
then
A /\ B <> (A /\ B) /\ D
by XBOOLE_0:def 4;
then A160:
card ((A /\ B) /\ D) <> card (A /\ B)
by A77, CARD_2:102, XBOOLE_1:17;
D on K13
by A156, INCSP_1:1;
then A161:
D c= K13
by A3, A6, Th10;
K13 in the
Lines of
(G_ (k,X))
;
then A162:
ex
R13 being
Subset of
X st
(
R13 = K13 &
card R13 = k + 1 )
by A14;
D on K12
by A157, INCSP_1:1;
then A163:
D c= K12
by A3, A6, Th10;
K12 in the
Lines of
(G_ (k,X))
;
then A164:
ex
R12 being
Subset of
X st
(
R12 = K12 &
card R12 = k + 1 )
by A14;
B on K12
by A157, INCSP_1:1;
then
B c= K12
by A3, A6, Th10;
then
B \/ D c= K12
by A163, XBOOLE_1:8;
then A165:
card (B \/ D) c= k + 1
by A164, CARD_1:11;
B <> D
by A126, A101, A148, A149, A150, A151;
then
k + 1
c= card (B \/ D)
by A74, A150, A151, Th1;
then
card (B \/ D) = (k - 1) + (2 * 1)
by A165, XBOOLE_0:def 10;
then A166:
card (B /\ D) = k - 1
by A29, A74, A155, Th2;
E on K13
by A156, INCSP_1:1;
then
E c= K13
by A3, A6, Th10;
then
E \/ D c= K13
by A161, XBOOLE_1:8;
then A167:
card (E \/ D) c= k + 1
by A162, CARD_1:11;
E <> D
by A126, A143, A148, A149, A150, A151;
then
k + 1
c= card (E \/ D)
by A120, A121, A150, A151, Th1;
then
card (E \/ D) = (k - 1) + (2 * 1)
by A167, XBOOLE_0:def 10;
then A168:
card (E /\ D) = k - 1
by A29, A120, A121, A155, Th2;
A169:
(
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, A142, A144, 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, A159, A166, A168, A160, 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 A170:
((A /\ B) /\ D) \/ {z1,z2,z4} c= D
by XBOOLE_1:8;
A171:
(
z4 in E \ (A /\ B) &
(A /\ B) /\ D c= A /\ B )
by A144, TARSKI:def 1, XBOOLE_1:17;
A172:
{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
object such that A173:
m in {z1,z2,z4} /\ ((A /\ B) /\ D)
by XBOOLE_0:def 1;
m in {z1,z2,z4}
by A173, XBOOLE_0:def 4;
then A174:
(
m = z1 or
m = z2 or
m = z4 )
by ENUMSET1:def 1;
m in (A /\ B) /\ D
by A173, XBOOLE_0:def 4;
hence
contradiction
by A89, A90, A123, A92, A171, A174, XBOOLE_0:def 5;
verum
end;
reconsider r =
card ((A /\ B) /\ D) as
Nat by A77;
A175:
not
z1 in (A /\ B) /\ D
by A124, 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 A169, ZFMISC_1:46;
then A176:
card (A /\ D) = r + 1
by A77, A175, CARD_2:41;
card {z1,z2,z4} = 3
by A57, A61, A64, A122, A91, A118, A133, A119, A121, A145, CARD_2:58;
then
card (((A /\ B) /\ D) \/ {z1,z2,z4}) = (k - 2) + 3
by A77, A159, A176, A172, CARD_2:40;
then
k + 1
c= k
by A150, A151, A170, 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 A177:
S1 = S
;
A178:
S1 is
STAR
by A70, A126, A88, A177;
then
S1 is
maximal_clique
by A3, A4, Th14;
then
S1 is
clique
;
hence
K is
STAR
by A12, A146, A177, A178;
verum
end;
reconsider k2 = k - 2 as Element of NAT by A3, NAT_1:21;
A179:
succ (Segm k2) = Segm (k2 + 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
A180:
1
+ 1
<= k + 1
by A9, XREAL_1:7;
A181:
card B = (k - 1) + 1
by A74;
A182:
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 A183:
C in K
and A184:
C on L
and A185:
A <> C
and A186:
B <> C
;
A187:
C c= L
by A3, A6, A184, Th10;
then
A \/ C c= L
by A68, XBOOLE_1:8;
then A188:
card (A \/ C) c= k + 1
by A66, CARD_1:11;
B \/ C c= L
by A71, A187, XBOOLE_1:8;
then A189:
card (B \/ C) c= k + 1
by A66, CARD_1:11;
C in the
Points of
(G_ (k,X))
;
then A190:
ex
C2 being
Subset of
X st
(
C2 = C &
card C2 = k )
by A7;
then
k + 1
c= card (B \/ C)
by A74, A186, Th1;
then
card (B \/ C) = (k - 1) + (2 * 1)
by A189, XBOOLE_0:def 10;
then A191:
card (B /\ C) = (k + 1) - 2
by A29, A190, A181, Th2;
k + 1
c= card (A \/ C)
by A76, A185, A190, Th1;
then
card (A \/ C) = (k - 1) + (2 * 1)
by A188, XBOOLE_0:def 10;
then A192:
card (A /\ C) = (k + 1) - 2
by A29, A190, A182, Th2;
A193:
card (A \/ B) = (k - 1) + (2 * 1)
by A73, A78, XBOOLE_0:def 10;
then A194:
A \/ B = L
by A68, A71, A66, A67, CARD_2:102, XBOOLE_1:8;
A195:
A \/ B c= (A \/ B) \/ C
by XBOOLE_1:7;
(A \/ B) \/ C c= L
by A72, A187, XBOOLE_1:8;
then A196:
card ((A \/ B) \/ C) = k + 1
by A193, A194, A195, XBOOLE_0:def 10;
A197:
(
card A = (k + 1) - 1 & 2
+ 1
<= k + 1 )
by A3, A76, XREAL_1:7;
consider T being
set such that A198:
T = { D where D is Subset of X : ( card D = k & D c= L ) }
;
card (A /\ B) = k - 1
by A29, A74, A193, A182, Th2;
then A199:
( (
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, A190, A192, A197, A191, A180, Th7;
A200:
K c= T
proof
let D2 be
object ;
TARSKI:def 3 ( not D2 in K or D2 in T )
assume that A201:
D2 in K
and A202:
not
D2 in T
;
contradiction
D2 in the
Points of
(G_ (k,X))
by A201;
then consider D1 being
Subset of
X such that A203:
D1 = D2
and A204:
card D1 = k
by A7;
consider D being
POINT of
(G_ (k,X)) such that A205:
D = D1
by A201, A203;
not
D c= L
by A198, A202, A203, A204, A205;
then consider x being
object such that A206:
x in D
and A207:
not
x in L
;
A208:
card {x} = 1
by CARD_1:30;
A209:
D is
finite
by A204, A205;
A210:
card D = (k - 1) + 1
by A204, A205;
{x} c= D
by A206, ZFMISC_1:31;
then A211:
card (D \ {x}) = k - 1
by A204, A205, A209, A208, CARD_2:44;
consider L13 being
LINE of
(G_ (k,X)) such that A212:
{C,D} on L13
by A13, A183, A201, A203, A205;
D on L13
by A212, INCSP_1:1;
then A213:
D c= L13
by A3, A6, Th10;
L13 in the
Lines of
(G_ (k,X))
;
then A214:
ex
L23 being
Subset of
X st
(
L23 = L13 &
card L23 = k + 1 )
by A14;
C on L13
by A212, INCSP_1:1;
then
C c= L13
by A3, A6, Th10;
then
C \/ D c= L13
by A213, XBOOLE_1:8;
then A215:
card (C \/ D) c= k + 1
by A214, CARD_1:11;
A216:
not
x in C
by A187, A207;
A217:
C /\ D c= D \ {x}
C <> D
by A187, A198, A202, A203, A204, A205;
then
k + 1
c= card (C \/ D)
by A190, A204, A205, Th1;
then
card (C \/ D) = (k - 1) + (2 * 1)
by A215, XBOOLE_0:def 10;
then
card (C /\ D) = k - 1
by A29, A190, A210, Th2;
then A220:
C /\ D = D \ {x}
by A209, A211, A217, CARD_2:102;
consider L12 being
LINE of
(G_ (k,X)) such that A221:
{B,D} on L12
by A13, A55, A62, A64, A201, A203, A205;
consider L11 being
LINE of
(G_ (k,X)) such that A222:
{A,D} on L11
by A13, A55, A59, A61, A201, A203, A205;
D on L11
by A222, INCSP_1:1;
then A223:
D c= L11
by A3, A6, Th10;
L11 in the
Lines of
(G_ (k,X))
;
then A224:
ex
L21 being
Subset of
X st
(
L21 = L11 &
card L21 = k + 1 )
by A14;
A on L11
by A222, INCSP_1:1;
then
A c= L11
by A3, A6, Th10;
then
A \/ D c= L11
by A223, XBOOLE_1:8;
then A225:
card (A \/ D) c= k + 1
by A224, CARD_1:11;
A226:
not
x in A
by A68, A207;
A227:
A /\ D c= D \ {x}
A <> D
by A68, A198, A202, A203, A204, A205;
then
k + 1
c= card (A \/ D)
by A76, A204, A205, Th1;
then A230:
card (A \/ D) = (k - 1) + (2 * 1)
by A225, XBOOLE_0:def 10;
then
card (A /\ D) = k - 1
by A29, A76, A210, Th2;
then A231:
A /\ D = D \ {x}
by A209, A211, A227, CARD_2:102;
D on L12
by A221, INCSP_1:1;
then A232:
D c= L12
by A3, A6, Th10;
L12 in the
Lines of
(G_ (k,X))
;
then A233:
ex
L22 being
Subset of
X st
(
L22 = L12 &
card L22 = k + 1 )
by A14;
B on L12
by A221, INCSP_1:1;
then
B c= L12
by A3, A6, Th10;
then
B \/ D c= L12
by A232, XBOOLE_1:8;
then A234:
card (B \/ D) c= k + 1
by A233, CARD_1:11;
A235:
not
x in B
by A71, A207;
A236:
B /\ D c= D \ {x}
B <> D
by A71, A198, A202, A203, A204, A205;
then
k + 1
c= card (B \/ D)
by A74, A204, A205, Th1;
then
card (B \/ D) = (k - 1) + (2 * 1)
by A234, XBOOLE_0:def 10;
then
card (B /\ D) = k - 1
by A29, A74, A210, Th2;
then
B /\ D = D \ {x}
by A209, A211, A236, CARD_2:102;
then
A /\ D = (A /\ D) /\ (B /\ D)
by A231;
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 A231, A220;
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, A210, A230, Th2;
then
k - 1
c= k2
by A196, A199, CARD_1:11, XBOOLE_1:17;
then
k - 1
in k - 1
by A179, 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 A239:
T1 = T
;
A240:
T1 is
TOP
by A66, A198, A239;
then
T1 is
maximal_clique
by A3, A4, Th14;
then
T1 is
clique
;
hence
K is
TOP
by A12, A200, A239, A240;
verum
end;
hence
( K is STAR or K is TOP )
by A81; verum