A1:
succ 0 = 0 + 1
;

A2: succ 2 = 2 + 1 ;

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 that

A3: 2 <= k and

A4: 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 )

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)); :: thesis: ( 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 ; :: thesis: ( 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 <> {}

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

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 )

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 )

A2: succ 2 = 2 + 1 ;

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 that

A3: 2 <= k and

A4: 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 )

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)); :: thesis: ( 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 ; :: thesis: ( 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

then
1 c= card K
by A1, A11, ORDINAL1:21;
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 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

then K c= U ;

hence contradiction by A12, A27, A24, A26; :: thesis: verum

end;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

proof

then
card A in card X
by A16, A18, A19, CARD_1:3;
assume
card A = card X
; :: thesis: contradiction

then k + 1 c= k by A4, A5, A18, A19;

then k in k by A10, ORDINAL1:21;

hence contradiction ; :: thesis: verum

end;then k + 1 c= k by A4, A5, A18, A19;

then k in k by A10, ORDINAL1:21;

hence contradiction ; :: thesis: verum

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

assume A27:
K = {}
; :: thesis: contradiction
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 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 ; :: thesis: verum

end;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 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 ; :: thesis: verum

then K c= U ;

hence contradiction by A12, A27, A24, A26; :: thesis: verum

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

succ 1 = 1 + 1
;
assume
card K = 1
; :: thesis: 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

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

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; :: thesis: verum

end;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

proof

card A c= card X
by A6, A15, A34;
assume
card A = card X
; :: thesis: contradiction

then k + 1 c= k by A4, A5, A34;

then k in k by A10, ORDINAL1:21;

hence contradiction ; :: thesis: verum

end;then k + 1 c= k by A4, A5, A34;

then k in k by A10, ORDINAL1:21;

hence contradiction ; :: thesis: verum

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

A in U
by A50, TARSKI:def 2;
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 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 ; :: thesis: verum

end;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 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 ; :: thesis: verum

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; :: thesis: verum

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

reconsider k2 = k - 2 as Element of NAT by A3, NAT_1:21;
A82:
card L <> card X

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} = {} )

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

A109: 3 c= card K

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 ) ; :: thesis: K is STAR

then A135: not E on L by A127, A118, A133, A119, A121;

A136: not card ((A \/ B) \/ E) = k + 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

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; :: thesis: verum

end;proof

card L c= card X
by A4, A5, A66;
assume
card L = card X
; :: thesis: contradiction

then k + 1 in k + 1 by A4, A8, A66, ORDINAL1:21;

hence contradiction ; :: thesis: verum

end;then k + 1 in k + 1 by A4, A8, A66, ORDINAL1:21;

hence contradiction ; :: thesis: verum

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} = {} )

proof

A87:
( card A = (k - 1) + 1 & card (A \/ B) = (k - 1) + (2 * 1) )
by A76, A73, A78, XBOOLE_0:def 10;
assume
( A /\ {x} <> {} or B /\ {x} <> {} )
; :: thesis: contradiction

then consider z1 being object such that

A86: ( z1 in A /\ {x} or z1 in B /\ {x} ) by XBOOLE_0:def 1;

( ( z1 in A & z1 in {x} ) or ( z1 in B & z1 in {x} ) ) by A86, XBOOLE_0:def 4;

hence contradiction by A84, TARSKI:def 1; :: thesis: verum

end;then consider z1 being object such that

A86: ( z1 in A /\ {x} or z1 in B /\ {x} ) by XBOOLE_0:def 1;

( ( z1 in A & z1 in {x} ) or ( z1 in B & z1 in {x} ) ) by A86, XBOOLE_0:def 4;

hence contradiction by A84, TARSKI:def 1; :: thesis: verum

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

A108:
( C <> A & C <> B )
by A84, A97, XBOOLE_1:11, ZFMISC_1:31;
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 that

A105: Z1 in {A,B,C} and

A106: Z2 in {A,B,C} ; :: thesis: 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 ; :: thesis: verum

end;assume that

A105: Z1 in {A,B,C} and

A106: Z2 in {A,B,C} ; :: thesis: 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 ; :: thesis: verum

A109: 3 c= card K

proof

card {A,B} <> card K
assume
not 3 c= card K
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

proof

then
card {A,B} in card K
by A54, A56, A58, A61, A64, CARD_1:3;
assume
card {A,B} = card K
; :: thesis: contradiction

then 3 in 3 by A2, A56, A58, A61, A64, A109, ORDINAL1:22;

hence contradiction ; :: thesis: verum

end;then 3 in 3 by A2, A56, A58, A61, A64, A109, ORDINAL1:22;

hence contradiction ; :: thesis: verum

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 ) ; :: thesis: K is STAR

then A135: not E on L by A127, A118, A133, A119, A121;

A136: not card ((A \/ B) \/ E) = k + 1

proof

E on K1
by A128, INCSP_1:1;
assume A137:
card ((A \/ B) \/ E) = k + 1
; :: thesis: contradiction

then ( A \/ B c= (A \/ B) \/ E & (A \/ B) \/ E is finite ) by XBOOLE_1:7;

then A138: A \/ B = (A \/ B) \/ E by A79, A137, CARD_2:102;

E c= (A \/ B) \/ E by XBOOLE_1:7;

then E c= L by A72, A138;

hence contradiction by A3, A6, A135, Th10; :: thesis: verum

end;then ( A \/ B c= (A \/ B) \/ E & (A \/ B) \/ E is finite ) by XBOOLE_1:7;

then A138: A \/ B = (A \/ B) \/ E by A79, A137, CARD_2:102;

E c= (A \/ B) \/ E by XBOOLE_1:7;

then E c= L by A72, A138;

hence contradiction by A3, A6, A135, Th10; :: thesis: verum

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

S c= the Points of (G_ (k,X))
assume
not K c= S
; :: thesis: 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 )

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

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 ; :: thesis: verum

end;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

then
( {z1,z2} c= D & {z4} c= D )
by ZFMISC_1:31, ZFMISC_1:32;
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 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; :: thesis: verum

end;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; :: thesis: verum

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

reconsider r = card ((A /\ B) /\ D) as Nat by A77;
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 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; :: thesis: verum

end;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; :: thesis: verum

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 ; :: thesis: verum

proof

then consider S1 being Subset of the Points of (G_ (k,X)) such that
let Z be object ; :: according to TARSKI:def 3 :: thesis: ( not Z in S or Z in the Points of (G_ (k,X)) )

assume Z in S ; :: thesis: Z in the Points of (G_ (k,X))

then ex Z1 being Subset of X st

( Z = Z1 & card Z1 = k & A /\ B c= Z1 ) by A126;

hence Z in the Points of (G_ (k,X)) by A7; :: thesis: verum

end;assume Z in S ; :: thesis: Z in the Points of (G_ (k,X))

then ex Z1 being Subset of X st

( Z = Z1 & card Z1 = k & A /\ B c= Z1 ) by A126;

hence Z in the Points of (G_ (k,X)) by A7; :: thesis: verum

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; :: thesis: verum

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

hence
( K is STAR or K is TOP )
by A81; :: thesis: verum
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 ) ; :: thesis: 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

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; :: thesis: verum

end;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 ) ; :: thesis: 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

T c= the Points of (G_ (k,X))
let D2 be object ; :: according to TARSKI:def 3 :: thesis: ( not D2 in K or D2 in T )

assume that

A201: D2 in K and

A202: not D2 in T ; :: thesis: 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}

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}

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}

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 ; :: thesis: verum

end;assume that

A201: D2 in K and

A202: not D2 in T ; :: thesis: 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}

proof

C <> D
by A187, A198, A202, A203, A204, A205;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in C /\ D or z in D \ {x} )

assume A218: z in C /\ D ; :: thesis: z in D \ {x}

then z <> x by A216, XBOOLE_0:def 4;

then A219: not z in {x} by TARSKI:def 1;

z in D by A218, XBOOLE_0:def 4;

hence z in D \ {x} by A219, XBOOLE_0:def 5; :: thesis: verum

end;assume A218: z in C /\ D ; :: thesis: z in D \ {x}

then z <> x by A216, XBOOLE_0:def 4;

then A219: not z in {x} by TARSKI:def 1;

z in D by A218, XBOOLE_0:def 4;

hence z in D \ {x} by A219, XBOOLE_0:def 5; :: thesis: verum

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}

proof

A <> D
by A68, A198, A202, A203, A204, A205;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in A /\ D or z in D \ {x} )

assume A228: z in A /\ D ; :: thesis: z in D \ {x}

then z <> x by A226, XBOOLE_0:def 4;

then A229: not z in {x} by TARSKI:def 1;

z in D by A228, XBOOLE_0:def 4;

hence z in D \ {x} by A229, XBOOLE_0:def 5; :: thesis: verum

end;assume A228: z in A /\ D ; :: thesis: z in D \ {x}

then z <> x by A226, XBOOLE_0:def 4;

then A229: not z in {x} by TARSKI:def 1;

z in D by A228, XBOOLE_0:def 4;

hence z in D \ {x} by A229, XBOOLE_0:def 5; :: thesis: verum

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}

proof

B <> D
by A71, A198, A202, A203, A204, A205;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in B /\ D or z in D \ {x} )

assume A237: z in B /\ D ; :: thesis: z in D \ {x}

then z <> x by A235, XBOOLE_0:def 4;

then A238: not z in {x} by TARSKI:def 1;

z in D by A237, XBOOLE_0:def 4;

hence z in D \ {x} by A238, XBOOLE_0:def 5; :: thesis: verum

end;assume A237: z in B /\ D ; :: thesis: z in D \ {x}

then z <> x by A235, XBOOLE_0:def 4;

then A238: not z in {x} by TARSKI:def 1;

z in D by A237, XBOOLE_0:def 4;

hence z in D \ {x} by A238, XBOOLE_0:def 5; :: thesis: verum

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 ; :: thesis: verum

proof

then consider T1 being Subset of the Points of (G_ (k,X)) such that
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in T or e in the Points of (G_ (k,X)) )

assume e in T ; :: thesis: e in the Points of (G_ (k,X))

then ex E being Subset of X st

( e = E & card E = k & E c= L ) by A198;

hence e in the Points of (G_ (k,X)) by A7; :: thesis: verum

end;assume e in T ; :: thesis: e in the Points of (G_ (k,X))

then ex E being Subset of X st

( e = E & card E = k & E c= L ) by A198;

hence e in the Points of (G_ (k,X)) by A7; :: thesis: verum

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; :: thesis: verum