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)) st ( K is STAR or K is TOP ) holds

K is maximal_clique

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)) st ( K is STAR or K is TOP ) holds

K is maximal_clique )

assume that

A1: 2 <= k and

A2: k + 2 c= card X ; :: thesis: for K being Subset of the Points of (G_ (k,X)) st ( K is STAR or K is TOP ) holds

K is maximal_clique

A3: k - 2 is Element of NAT by A1, NAT_1:21;

then reconsider k2 = k - 2 as Nat ;

let K be Subset of the Points of (G_ (k,X)); :: thesis: ( ( K is STAR or K is TOP ) implies K is maximal_clique )

A4: succ (Segm k) = Segm (k + 1) by NAT_1:38;

A5: succ (Segm (k + 1)) = Segm ((k + 1) + 1) by NAT_1:38;

k + 1 <= k + 2 by XREAL_1:7;

then Segm (k + 1) c= Segm (k + 2) by NAT_1:39;

then A6: k + 1 c= card X by A2;

then A7: the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k } by A1, Def1;

A8: the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 } by A1, A6, Def1;

reconsider k1 = k - 1 as Element of NAT by A1, NAT_1:21, XXREAL_0:2;

A9: succ (Segm k1) = Segm (k1 + 1) by NAT_1:38;

A10: ( K is STAR implies K is maximal_clique )

( K is TOP implies K is maximal_clique )

for K being Subset of the Points of (G_ (k,X)) st ( K is STAR or K is TOP ) holds

K is maximal_clique

let X be non empty set ; :: thesis: ( 2 <= k & k + 2 c= card X implies for K being Subset of the Points of (G_ (k,X)) st ( K is STAR or K is TOP ) holds

K is maximal_clique )

assume that

A1: 2 <= k and

A2: k + 2 c= card X ; :: thesis: for K being Subset of the Points of (G_ (k,X)) st ( K is STAR or K is TOP ) holds

K is maximal_clique

A3: k - 2 is Element of NAT by A1, NAT_1:21;

then reconsider k2 = k - 2 as Nat ;

let K be Subset of the Points of (G_ (k,X)); :: thesis: ( ( K is STAR or K is TOP ) implies K is maximal_clique )

A4: succ (Segm k) = Segm (k + 1) by NAT_1:38;

A5: succ (Segm (k + 1)) = Segm ((k + 1) + 1) by NAT_1:38;

k + 1 <= k + 2 by XREAL_1:7;

then Segm (k + 1) c= Segm (k + 2) by NAT_1:39;

then A6: k + 1 c= card X by A2;

then A7: the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k } by A1, Def1;

A8: the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 } by A1, A6, Def1;

reconsider k1 = k - 1 as Element of NAT by A1, NAT_1:21, XXREAL_0:2;

A9: succ (Segm k1) = Segm (k1 + 1) by NAT_1:38;

A10: ( K is STAR implies K is maximal_clique )

proof

A76:
succ 0 = 0 + 1
;
assume
K is STAR
; :: thesis: K is maximal_clique

then consider S being Subset of X such that

A11: card S = k - 1 and

A12: K = { A where A is Subset of X : ( card A = k & S c= A ) } ;

A13: S is finite by A1, A11, NAT_1:21, XXREAL_0:2;

A14: for U being Subset of the Points of (G_ (k,X)) st U is clique & K c= U holds

U = K

end;then consider S being Subset of X such that

A11: card S = k - 1 and

A12: K = { A where A is Subset of X : ( card A = k & S c= A ) } ;

A13: S is finite by A1, A11, NAT_1:21, XXREAL_0:2;

A14: for U being Subset of the Points of (G_ (k,X)) st U is clique & K c= U holds

U = K

proof

K is clique
A15:
succ (Segm k2) = Segm (k2 + 1)
by NAT_1:38;

let U be Subset of the Points of (G_ (k,X)); :: thesis: ( U is clique & K c= U implies U = K )

assume that

A16: U is clique and

A17: K c= U and

A18: U <> K ; :: thesis: contradiction

not U c= K by A17, A18, XBOOLE_0:def 10;

then consider A being object such that

A19: A in U and

A20: not A in K ;

reconsider A = A as set by TARSKI:1;

consider A2 being POINT of (G_ (k,X)) such that

A21: A2 = A by A19;

card (S /\ A) c= k - 1 by A11, CARD_1:11, XBOOLE_1:17;

then card (S /\ A) in succ k1 by ORDINAL1:22;

then A22: ( card (S /\ A) in succ (k - 2) or card (S /\ A) = k - 1 ) by A15, ORDINAL1:8;

A23: ( S /\ A c= S & S /\ A c= A ) by XBOOLE_1:17;

A in the Points of (G_ (k,X)) by A19;

then consider A1 being Subset of X such that

A24: ( A1 = A & card A1 = k ) by A7;

not S c= A by A12, A20, A24;

then A25: card (S /\ A) c= k - 2 by A3, A11, A13, A23, A22, CARD_2:102, ORDINAL1:22;

A26: not X \ (A \/ S) <> {}

then card S in Segm k by A11, NAT_1:44;

then card S in card A by A24;

then A \ S <> {} by CARD_1:68;

then consider x being object such that

A45: x in A \ S by XBOOLE_0:def 1;

not x in S by A45, XBOOLE_0:def 5;

then A46: card (S \/ {x}) = (k - 1) + 1 by A11, A13, CARD_2:41;

A47: {x} c= A by A45, ZFMISC_1:31;

x in A by A45;

then A48: {x} c= X by A24, ZFMISC_1:31;

then A49: S \/ {x} c= X by XBOOLE_1:8;

not X \ (A \/ S) = {}

end;let U be Subset of the Points of (G_ (k,X)); :: thesis: ( U is clique & K c= U implies U = K )

assume that

A16: U is clique and

A17: K c= U and

A18: U <> K ; :: thesis: contradiction

not U c= K by A17, A18, XBOOLE_0:def 10;

then consider A being object such that

A19: A in U and

A20: not A in K ;

reconsider A = A as set by TARSKI:1;

consider A2 being POINT of (G_ (k,X)) such that

A21: A2 = A by A19;

card (S /\ A) c= k - 1 by A11, CARD_1:11, XBOOLE_1:17;

then card (S /\ A) in succ k1 by ORDINAL1:22;

then A22: ( card (S /\ A) in succ (k - 2) or card (S /\ A) = k - 1 ) by A15, ORDINAL1:8;

A23: ( S /\ A c= S & S /\ A c= A ) by XBOOLE_1:17;

A in the Points of (G_ (k,X)) by A19;

then consider A1 being Subset of X such that

A24: ( A1 = A & card A1 = k ) by A7;

not S c= A by A12, A20, A24;

then A25: card (S /\ A) c= k - 2 by A3, A11, A13, A23, A22, CARD_2:102, ORDINAL1:22;

A26: not X \ (A \/ S) <> {}

proof

k1 < k1 + 1
by NAT_1:13;
A27:
succ (Segm k2) = Segm (k2 + 1)
by NAT_1:38;

assume X \ (A \/ S) <> {} ; :: thesis: contradiction

then consider y being object such that

A28: y in X \ (A \/ S) by XBOOLE_0:def 1;

A29: not y in A \/ S by A28, XBOOLE_0:def 5;

then A30: not y in S by XBOOLE_0:def 3;

then A31: card (S \/ {y}) = (k - 1) + 1 by A11, A13, CARD_2:41;

A32: {y} c= X by A28, ZFMISC_1:31;

then S \/ {y} c= X by XBOOLE_1:8;

then S \/ {y} in the Points of (G_ (k,X)) by A7, A31;

then consider B being POINT of (G_ (k,X)) such that

A33: B = S \/ {y} ;

A34: not y in A by A29, XBOOLE_0:def 3;

A /\ B c= A /\ S

then card (A /\ B) c= k - 2 by A25;

then A37: card (A /\ B) in k - 1 by A27, ORDINAL1:22;

A38: for L being LINE of (G_ (k,X)) holds not {A2,B} on L

B c= X by A32, A33, XBOOLE_1:8;

then B in K by A12, A31, A33, A44;

hence contradiction by A16, A17, A19, A21, A38; :: thesis: verum

end;assume X \ (A \/ S) <> {} ; :: thesis: contradiction

then consider y being object such that

A28: y in X \ (A \/ S) by XBOOLE_0:def 1;

A29: not y in A \/ S by A28, XBOOLE_0:def 5;

then A30: not y in S by XBOOLE_0:def 3;

then A31: card (S \/ {y}) = (k - 1) + 1 by A11, A13, CARD_2:41;

A32: {y} c= X by A28, ZFMISC_1:31;

then S \/ {y} c= X by XBOOLE_1:8;

then S \/ {y} in the Points of (G_ (k,X)) by A7, A31;

then consider B being POINT of (G_ (k,X)) such that

A33: B = S \/ {y} ;

A34: not y in A by A29, XBOOLE_0:def 3;

A /\ B c= A /\ S

proof

then
card (A /\ B) c= card (A /\ S)
by CARD_1:11;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A /\ B or a in A /\ S )

assume A35: a in A /\ B ; :: thesis: a in A /\ S

then a in S \/ {y} by A33, XBOOLE_0:def 4;

then A36: ( a in S or a in {y} ) by XBOOLE_0:def 3;

a in A by A35, XBOOLE_0:def 4;

hence a in A /\ S by A34, A36, TARSKI:def 1, XBOOLE_0:def 4; :: thesis: verum

end;assume A35: a in A /\ B ; :: thesis: a in A /\ S

then a in S \/ {y} by A33, XBOOLE_0:def 4;

then A36: ( a in S or a in {y} ) by XBOOLE_0:def 3;

a in A by A35, XBOOLE_0:def 4;

hence a in A /\ S by A34, A36, TARSKI:def 1, XBOOLE_0:def 4; :: thesis: verum

then card (A /\ B) c= k - 2 by A25;

then A37: card (A /\ B) in k - 1 by A27, ORDINAL1:22;

A38: for L being LINE of (G_ (k,X)) holds not {A2,B} on L

proof

A44:
S c= B
by A33, XBOOLE_1:7;
A <> B
by A33, A34, XBOOLE_1:7, ZFMISC_1:31;

then A39: k + 1 c= card (A \/ B) by A24, A31, A33, Th1;

assume ex L being LINE of (G_ (k,X)) st {A2,B} on L ; :: thesis: contradiction

then consider L being LINE of (G_ (k,X)) such that

A40: {A2,B} on L ;

B on L by A40, INCSP_1:1;

then A41: B c= L by A1, A6, Th10;

L in the Lines of (G_ (k,X)) ;

then A42: ex L1 being Subset of X st

( L = L1 & card L1 = k + 1 ) by A8;

A2 on L by A40, INCSP_1:1;

then A c= L by A1, A6, A21, Th10;

then A \/ B c= L by A41, XBOOLE_1:8;

then card (A \/ B) c= k + 1 by A42, CARD_1:11;

then A43: card (A \/ B) = (k - 1) + (2 * 1) by A39, XBOOLE_0:def 10;

card B = (k - 1) + 1 by A11, A13, A30, A33, CARD_2:41;

then card (A /\ B) = k1 by A24, A43, Th2;

hence contradiction by A37; :: thesis: verum

end;then A39: k + 1 c= card (A \/ B) by A24, A31, A33, Th1;

assume ex L being LINE of (G_ (k,X)) st {A2,B} on L ; :: thesis: contradiction

then consider L being LINE of (G_ (k,X)) such that

A40: {A2,B} on L ;

B on L by A40, INCSP_1:1;

then A41: B c= L by A1, A6, Th10;

L in the Lines of (G_ (k,X)) ;

then A42: ex L1 being Subset of X st

( L = L1 & card L1 = k + 1 ) by A8;

A2 on L by A40, INCSP_1:1;

then A c= L by A1, A6, A21, Th10;

then A \/ B c= L by A41, XBOOLE_1:8;

then card (A \/ B) c= k + 1 by A42, CARD_1:11;

then A43: card (A \/ B) = (k - 1) + (2 * 1) by A39, XBOOLE_0:def 10;

card B = (k - 1) + 1 by A11, A13, A30, A33, CARD_2:41;

then card (A /\ B) = k1 by A24, A43, Th2;

hence contradiction by A37; :: thesis: verum

B c= X by A32, A33, XBOOLE_1:8;

then B in K by A12, A31, A33, A44;

hence contradiction by A16, A17, A19, A21, A38; :: thesis: verum

then card S in Segm k by A11, NAT_1:44;

then card S in card A by A24;

then A \ S <> {} by CARD_1:68;

then consider x being object such that

A45: x in A \ S by XBOOLE_0:def 1;

not x in S by A45, XBOOLE_0:def 5;

then A46: card (S \/ {x}) = (k - 1) + 1 by A11, A13, CARD_2:41;

A47: {x} c= A by A45, ZFMISC_1:31;

x in A by A45;

then A48: {x} c= X by A24, ZFMISC_1:31;

then A49: S \/ {x} c= X by XBOOLE_1:8;

not X \ (A \/ S) = {}

proof

hence
contradiction
by A26; :: thesis: verum
assume
X \ (A \/ S) = {}
; :: thesis: contradiction

then A50: X c= A \/ S by XBOOLE_1:37;

S \/ {x} in the Points of (G_ (k,X)) by A7, A46, A49;

then consider B being POINT of (G_ (k,X)) such that

A51: B = S \/ {x} ;

A \/ B = (A \/ S) \/ {x} by A51, XBOOLE_1:4;

then A52: A \/ B = A \/ S by A47, XBOOLE_1:10, XBOOLE_1:12;

A \/ S c= X by A24, XBOOLE_1:8;

then A53: A \/ S = X by A50, XBOOLE_0:def 10;

A54: for L being LINE of (G_ (k,X)) holds not {A2,B} on L

then B in K by A12, A46, A51;

hence contradiction by A16, A17, A19, A21, A54; :: thesis: verum

end;then A50: X c= A \/ S by XBOOLE_1:37;

S \/ {x} in the Points of (G_ (k,X)) by A7, A46, A49;

then consider B being POINT of (G_ (k,X)) such that

A51: B = S \/ {x} ;

A \/ B = (A \/ S) \/ {x} by A51, XBOOLE_1:4;

then A52: A \/ B = A \/ S by A47, XBOOLE_1:10, XBOOLE_1:12;

A \/ S c= X by A24, XBOOLE_1:8;

then A53: A \/ S = X by A50, XBOOLE_0:def 10;

A54: for L being LINE of (G_ (k,X)) holds not {A2,B} on L

proof

( S c= B & B c= X )
by A48, A51, XBOOLE_1:8, XBOOLE_1:10;
assume
ex L being LINE of (G_ (k,X)) st {A2,B} on L
; :: thesis: contradiction

then consider L being LINE of (G_ (k,X)) such that

A55: {A2,B} on L ;

B on L by A55, INCSP_1:1;

then A56: B c= L by A1, A6, Th10;

A2 on L by A55, INCSP_1:1;

then A c= L by A1, A6, A21, Th10;

then A \/ B c= L by A56, XBOOLE_1:8;

then card (A \/ B) c= card L by CARD_1:11;

then A57: k + 2 c= card L by A2, A53, A52;

L in the Lines of (G_ (k,X)) ;

then ex L1 being Subset of X st

( L = L1 & card L1 = k + 1 ) by A8;

then k + 1 in k + 1 by A5, A57, ORDINAL1:21;

hence contradiction ; :: thesis: verum

end;then consider L being LINE of (G_ (k,X)) such that

A55: {A2,B} on L ;

B on L by A55, INCSP_1:1;

then A56: B c= L by A1, A6, Th10;

A2 on L by A55, INCSP_1:1;

then A c= L by A1, A6, A21, Th10;

then A \/ B c= L by A56, XBOOLE_1:8;

then card (A \/ B) c= card L by CARD_1:11;

then A57: k + 2 c= card L by A2, A53, A52;

L in the Lines of (G_ (k,X)) ;

then ex L1 being Subset of X st

( L = L1 & card L1 = k + 1 ) by A8;

then k + 1 in k + 1 by A5, A57, ORDINAL1:21;

hence contradiction ; :: thesis: verum

then B in K by A12, A46, A51;

hence contradiction by A16, A17, A19, A21, A54; :: thesis: verum

proof

hence
K is maximal_clique
by A14; :: thesis: verum
let A, B be POINT of (G_ (k,X)); :: according to COMBGRAS:def 2 :: thesis: ( A in K & B in K implies ex L being LINE of (G_ (k,X)) st {A,B} on L )

assume that

A58: A in K and

A59: B in K ; :: thesis: ex L being LINE of (G_ (k,X)) st {A,B} on L

A60: ex A1 being Subset of X st

( A1 = A & card A1 = k & S c= A1 ) by A12, A58;

then A61: A is finite ;

A62: ex B1 being Subset of X st

( B1 = B & card B1 = k & S c= B1 ) by A12, A59;

then S c= A /\ B by A60, XBOOLE_1:19;

then k - 1 c= card (A /\ B) by A11, CARD_1:11;

then k1 in succ (card (A /\ B)) by ORDINAL1:22;

then ( card (A /\ B) = k - 1 or k - 1 in card (A /\ B) ) by ORDINAL1:8;

then A63: ( card (A /\ B) = k - 1 or k c= card (A /\ B) ) by A9, ORDINAL1:21;

A64: B is finite by A62;

A65: ( card (A /\ B) = k implies ex L being LINE of (G_ (k,X)) st {A,B} on L )

hence ex L being LINE of (G_ (k,X)) st {A,B} on L by A63, A71, A65, XBOOLE_0:def 10; :: thesis: verum

end;assume that

A58: A in K and

A59: B in K ; :: thesis: ex L being LINE of (G_ (k,X)) st {A,B} on L

A60: ex A1 being Subset of X st

( A1 = A & card A1 = k & S c= A1 ) by A12, A58;

then A61: A is finite ;

A62: ex B1 being Subset of X st

( B1 = B & card B1 = k & S c= B1 ) by A12, A59;

then S c= A /\ B by A60, XBOOLE_1:19;

then k - 1 c= card (A /\ B) by A11, CARD_1:11;

then k1 in succ (card (A /\ B)) by ORDINAL1:22;

then ( card (A /\ B) = k - 1 or k - 1 in card (A /\ B) ) by ORDINAL1:8;

then A63: ( card (A /\ B) = k - 1 or k c= card (A /\ B) ) by A9, ORDINAL1:21;

A64: B is finite by A62;

A65: ( card (A /\ B) = k implies ex L being LINE of (G_ (k,X)) st {A,B} on L )

proof

A71:
( card (A /\ B) = k - 1 implies ex L being LINE of (G_ (k,X)) st {A,B} on L )
A66:
card A <> card X

then card A in card X by A66, CARD_1:3;

then X \ A <> {} by CARD_1:68;

then consider x being object such that

A67: x in X \ A by XBOOLE_0:def 1;

{x} c= X by A67, ZFMISC_1:31;

then A68: A \/ {x} c= X by A60, XBOOLE_1:8;

not x in A by A67, XBOOLE_0:def 5;

then card (A \/ {x}) = k + 1 by A60, A61, CARD_2:41;

then A \/ {x} in the Lines of (G_ (k,X)) by A8, A68;

then consider L being LINE of (G_ (k,X)) such that

A69: L = A \/ {x} ;

assume card (A /\ B) = k ; :: thesis: ex L being LINE of (G_ (k,X)) st {A,B} on L

then ( A /\ B = A & A /\ B = B ) by A60, A62, A61, A64, CARD_2:102, XBOOLE_1:17;

then B c= A \/ {x} by XBOOLE_1:7;

then A70: B on L by A1, A6, A69, Th10;

A c= A \/ {x} by XBOOLE_1:7;

then A on L by A1, A6, A69, Th10;

then {A,B} on L by A70, INCSP_1:1;

hence ex L being LINE of (G_ (k,X)) st {A,B} on L ; :: thesis: verum

end;proof

card A c= card X
by A60, CARD_1:11;
assume
card A = card X
; :: thesis: contradiction

then k in k by A6, A4, A60, ORDINAL1:21;

hence contradiction ; :: thesis: verum

end;then k in k by A6, A4, A60, ORDINAL1:21;

hence contradiction ; :: thesis: verum

then card A in card X by A66, CARD_1:3;

then X \ A <> {} by CARD_1:68;

then consider x being object such that

A67: x in X \ A by XBOOLE_0:def 1;

{x} c= X by A67, ZFMISC_1:31;

then A68: A \/ {x} c= X by A60, XBOOLE_1:8;

not x in A by A67, XBOOLE_0:def 5;

then card (A \/ {x}) = k + 1 by A60, A61, CARD_2:41;

then A \/ {x} in the Lines of (G_ (k,X)) by A8, A68;

then consider L being LINE of (G_ (k,X)) such that

A69: L = A \/ {x} ;

assume card (A /\ B) = k ; :: thesis: ex L being LINE of (G_ (k,X)) st {A,B} on L

then ( A /\ B = A & A /\ B = B ) by A60, A62, A61, A64, CARD_2:102, XBOOLE_1:17;

then B c= A \/ {x} by XBOOLE_1:7;

then A70: B on L by A1, A6, A69, Th10;

A c= A \/ {x} by XBOOLE_1:7;

then A on L by A1, A6, A69, Th10;

then {A,B} on L by A70, INCSP_1:1;

hence ex L being LINE of (G_ (k,X)) st {A,B} on L ; :: thesis: verum

proof

card (A /\ B) c= k
by A60, CARD_1:11, XBOOLE_1:17;
A72:
A \/ B c= X
by A60, A62, XBOOLE_1:8;

assume A73: card (A /\ B) = k - 1 ; :: thesis: ex L being LINE of (G_ (k,X)) st {A,B} on L

card A = (k - 1) + 1 by A60;

then card (A \/ B) = k1 + (2 * 1) by A62, A73, Th2;

then A \/ B in the Lines of (G_ (k,X)) by A8, A72;

then consider L being LINE of (G_ (k,X)) such that

A74: L = A \/ B ;

B c= A \/ B by XBOOLE_1:7;

then A75: B on L by A1, A6, A74, Th10;

A c= A \/ B by XBOOLE_1:7;

then A on L by A1, A6, A74, Th10;

then {A,B} on L by A75, INCSP_1:1;

hence ex L being LINE of (G_ (k,X)) st {A,B} on L ; :: thesis: verum

end;assume A73: card (A /\ B) = k - 1 ; :: thesis: ex L being LINE of (G_ (k,X)) st {A,B} on L

card A = (k - 1) + 1 by A60;

then card (A \/ B) = k1 + (2 * 1) by A62, A73, Th2;

then A \/ B in the Lines of (G_ (k,X)) by A8, A72;

then consider L being LINE of (G_ (k,X)) such that

A74: L = A \/ B ;

B c= A \/ B by XBOOLE_1:7;

then A75: B on L by A1, A6, A74, Th10;

A c= A \/ B by XBOOLE_1:7;

then A on L by A1, A6, A74, Th10;

then {A,B} on L by A75, INCSP_1:1;

hence ex L being LINE of (G_ (k,X)) st {A,B} on L ; :: thesis: verum

hence ex L being LINE of (G_ (k,X)) st {A,B} on L by A63, A71, A65, XBOOLE_0:def 10; :: thesis: verum

( K is TOP implies K is maximal_clique )

proof

hence
( ( K is STAR or K is TOP ) implies K is maximal_clique )
by A10; :: thesis: verum
assume
K is TOP
; :: thesis: K is maximal_clique

then consider S being Subset of X such that

A77: card S = k + 1 and

A78: K = { A where A is Subset of X : ( card A = k & A c= S ) } ;

reconsider S = S as finite set by A77;

A79: for U being Subset of the Points of (G_ (k,X)) st U is clique & K c= U holds

U = K

end;then consider S being Subset of X such that

A77: card S = k + 1 and

A78: K = { A where A is Subset of X : ( card A = k & A c= S ) } ;

reconsider S = S as finite set by A77;

A79: for U being Subset of the Points of (G_ (k,X)) st U is clique & K c= U holds

U = K

proof

K is clique
A80:
k - 2 <= (k - 2) + 1
by A3, NAT_1:11;

let U be Subset of the Points of (G_ (k,X)); :: thesis: ( U is clique & K c= U implies U = K )

assume that

A81: U is clique and

A82: K c= U and

A83: U <> K ; :: thesis: contradiction

not U c= K by A82, A83, XBOOLE_0:def 10;

then consider A being object such that

A84: A in U and

A85: not A in K ;

reconsider A = A as set by TARSKI:1;

consider A2 being POINT of (G_ (k,X)) such that

A86: A2 = A by A84;

A in the Points of (G_ (k,X)) by A84;

then A87: ex A1 being Subset of X st

( A1 = A & card A1 = k ) by A7;

then reconsider A = A as finite set ;

A88: card A <> card S by A77, A87;

A89: not A c= S by A78, A85, A87;

then consider x being object such that

A90: x in A and

A91: not x in S ;

k <= k + 1 by NAT_1:11;

then Segm (card A) c= Segm (card S) by A77, A87, NAT_1:39;

then card A in card S by A88, CARD_1:3;

then A92: S \ A <> {} by CARD_1:68;

2 c= card (S \ A)

A95: B1 c= S \ A and

A96: card B1 = 2 by CARD_FIL:36;

A97: B1 c= S by A95, XBOOLE_1:106;

then A98: not x in B1 by A91;

card (S \ B1) = (k + 1) - 2 by A77, A95, A96, CARD_2:44, XBOOLE_1:106;

then Segm k2 c= Segm (card (S \ B1)) by A80, NAT_1:39;

then consider B2 being set such that

A99: B2 c= S \ B1 and

A100: card B2 = k - 2 by CARD_FIL:36;

A101: card (B1 \/ B2) = 2 + (k - 2) by A95, A96, A99, A100, CARD_2:40, XBOOLE_1:106;

S \ B1 c= X by XBOOLE_1:1;

then A102: B2 c= X by A99;

S \ A c= X by XBOOLE_1:1;

then B1 c= X by A95;

then A103: B1 \/ B2 c= X by A102, XBOOLE_1:8;

then B1 \/ B2 in the Points of (G_ (k,X)) by A7, A101;

then consider B being POINT of (G_ (k,X)) such that

A104: B = B1 \/ B2 ;

B1 misses A by A95, XBOOLE_1:106;

then A105: B1 /\ A = {} by XBOOLE_0:def 7;

B2 c= S by A99, XBOOLE_1:106;

then A106: B1 \/ B2 c= S by A97, XBOOLE_1:8;

then A107: not x in B1 \/ B2 by A91;

A108: A /\ B c= A \/ B by XBOOLE_1:29;

A109: k + 2 c= card (A \/ B)

hence contradiction by A81, A82, A84, A86, A119; :: thesis: verum

end;let U be Subset of the Points of (G_ (k,X)); :: thesis: ( U is clique & K c= U implies U = K )

assume that

A81: U is clique and

A82: K c= U and

A83: U <> K ; :: thesis: contradiction

not U c= K by A82, A83, XBOOLE_0:def 10;

then consider A being object such that

A84: A in U and

A85: not A in K ;

reconsider A = A as set by TARSKI:1;

consider A2 being POINT of (G_ (k,X)) such that

A86: A2 = A by A84;

A in the Points of (G_ (k,X)) by A84;

then A87: ex A1 being Subset of X st

( A1 = A & card A1 = k ) by A7;

then reconsider A = A as finite set ;

A88: card A <> card S by A77, A87;

A89: not A c= S by A78, A85, A87;

then consider x being object such that

A90: x in A and

A91: not x in S ;

k <= k + 1 by NAT_1:11;

then Segm (card A) c= Segm (card S) by A77, A87, NAT_1:39;

then card A in card S by A88, CARD_1:3;

then A92: S \ A <> {} by CARD_1:68;

2 c= card (S \ A)

proof

then consider B1 being set such that
A93:
not card (S \ A) = 1

then card (S \ A) in succ 1 by ORDINAL1:16;

then ( card (S \ A) in 1 or card (S \ A) = 1 ) by ORDINAL1:8;

then ( card (S \ A) c= 0 or card (S \ A) = 1 ) by A76, ORDINAL1:22;

hence contradiction by A92, A93; :: thesis: verum

end;proof

assume
not 2 c= card (S \ A)
; :: thesis: contradiction
assume
card (S \ A) = 1
; :: thesis: contradiction

then A94: card (S \ (S \ A)) = (k + 1) - 1 by A77, CARD_2:44;

( S \ (S \ A) = S /\ A & S /\ A c= S ) by XBOOLE_1:17, XBOOLE_1:48;

hence contradiction by A87, A89, A94, CARD_2:102, XBOOLE_1:17; :: thesis: verum

end;then A94: card (S \ (S \ A)) = (k + 1) - 1 by A77, CARD_2:44;

( S \ (S \ A) = S /\ A & S /\ A c= S ) by XBOOLE_1:17, XBOOLE_1:48;

hence contradiction by A87, A89, A94, CARD_2:102, XBOOLE_1:17; :: thesis: verum

then card (S \ A) in succ 1 by ORDINAL1:16;

then ( card (S \ A) in 1 or card (S \ A) = 1 ) by ORDINAL1:8;

then ( card (S \ A) c= 0 or card (S \ A) = 1 ) by A76, ORDINAL1:22;

hence contradiction by A92, A93; :: thesis: verum

A95: B1 c= S \ A and

A96: card B1 = 2 by CARD_FIL:36;

A97: B1 c= S by A95, XBOOLE_1:106;

then A98: not x in B1 by A91;

card (S \ B1) = (k + 1) - 2 by A77, A95, A96, CARD_2:44, XBOOLE_1:106;

then Segm k2 c= Segm (card (S \ B1)) by A80, NAT_1:39;

then consider B2 being set such that

A99: B2 c= S \ B1 and

A100: card B2 = k - 2 by CARD_FIL:36;

A101: card (B1 \/ B2) = 2 + (k - 2) by A95, A96, A99, A100, CARD_2:40, XBOOLE_1:106;

S \ B1 c= X by XBOOLE_1:1;

then A102: B2 c= X by A99;

S \ A c= X by XBOOLE_1:1;

then B1 c= X by A95;

then A103: B1 \/ B2 c= X by A102, XBOOLE_1:8;

then B1 \/ B2 in the Points of (G_ (k,X)) by A7, A101;

then consider B being POINT of (G_ (k,X)) such that

A104: B = B1 \/ B2 ;

B1 misses A by A95, XBOOLE_1:106;

then A105: B1 /\ A = {} by XBOOLE_0:def 7;

B2 c= S by A99, XBOOLE_1:106;

then A106: B1 \/ B2 c= S by A97, XBOOLE_1:8;

then A107: not x in B1 \/ B2 by A91;

A108: A /\ B c= A \/ B by XBOOLE_1:29;

A109: k + 2 c= card (A \/ B)

proof

A119:
for L being LINE of (G_ (k,X)) holds not {A2,B} on L
A110:
{x} \/ B1 misses A /\ B

then {x} c= A \/ B by XBOOLE_1:10;

then A113: (A /\ B) \/ {x} c= A \/ B by A108, XBOOLE_1:8;

B1 c= B by A104, XBOOLE_1:10;

then B1 c= A \/ B by XBOOLE_1:10;

then ((A /\ B) \/ {x}) \/ B1 c= A \/ B by A113, XBOOLE_1:8;

then (A /\ B) \/ ({x} \/ B1) c= A \/ B by XBOOLE_1:4;

then A114: card ((A /\ B) \/ ({x} \/ B1)) c= card (A \/ B) by CARD_1:11;

assume not k + 2 c= card (A \/ B) ; :: thesis: contradiction

then A115: card (A \/ B) in succ (k + 1) by A5, ORDINAL1:16;

then A116: card (A \/ B) c= k + 1 by ORDINAL1:22;

( card (A \/ B) = k + 1 or ( card (A \/ B) in succ k & A c= A \/ B ) ) by A4, A115, ORDINAL1:8, XBOOLE_1:7;

then ( card (A \/ B) = k + 1 or ( card (A \/ B) c= k & k c= card (A \/ B) ) ) by A87, CARD_1:11, ORDINAL1:22;

then A117: ( card (A \/ B) = (k - 1) + (2 * 1) or card (A \/ B) = k + (2 * 0) ) by XBOOLE_0:def 10;

card A = (k - 1) + 1 by A87;

then A118: ( card (A /\ B) = k1 or card (A /\ B) = k ) by A101, A104, A117, Th2;

card ({x} \/ B1) = 2 + 1 by A95, A96, A98, CARD_2:41;

then ( card ((A /\ B) \/ ({x} \/ B1)) = (k - 1) + 3 or card ((A /\ B) \/ ({x} \/ B1)) = k + 3 ) by A95, A110, A118, CARD_2:40;

then ( Segm (k + 2) c= Segm (k + 1) or Segm (k + 3) c= Segm (k + 1) ) by A116, A114;

then ( k + 1 in k + 1 or k + 3 <= k + 1 ) by A5, NAT_1:39, ORDINAL1:21;

hence contradiction by XREAL_1:6; :: thesis: verum

end;proof

{x} c= A
by A90, ZFMISC_1:31;
assume
not {x} \/ B1 misses A /\ B
; :: thesis: contradiction

then ({x} \/ B1) /\ (A /\ B) <> {} by XBOOLE_0:def 7;

then consider y being object such that

A111: y in ({x} \/ B1) /\ (A /\ B) by XBOOLE_0:def 1;

y in A /\ B by A111, XBOOLE_0:def 4;

then A112: ( y in A & y in B ) by XBOOLE_0:def 4;

y in {x} \/ B1 by A111, XBOOLE_0:def 4;

then ( y in {x} or y in B1 ) by XBOOLE_0:def 3;

hence contradiction by A104, A107, A105, A112, TARSKI:def 1, XBOOLE_0:def 4; :: thesis: verum

end;then ({x} \/ B1) /\ (A /\ B) <> {} by XBOOLE_0:def 7;

then consider y being object such that

A111: y in ({x} \/ B1) /\ (A /\ B) by XBOOLE_0:def 1;

y in A /\ B by A111, XBOOLE_0:def 4;

then A112: ( y in A & y in B ) by XBOOLE_0:def 4;

y in {x} \/ B1 by A111, XBOOLE_0:def 4;

then ( y in {x} or y in B1 ) by XBOOLE_0:def 3;

hence contradiction by A104, A107, A105, A112, TARSKI:def 1, XBOOLE_0:def 4; :: thesis: verum

then {x} c= A \/ B by XBOOLE_1:10;

then A113: (A /\ B) \/ {x} c= A \/ B by A108, XBOOLE_1:8;

B1 c= B by A104, XBOOLE_1:10;

then B1 c= A \/ B by XBOOLE_1:10;

then ((A /\ B) \/ {x}) \/ B1 c= A \/ B by A113, XBOOLE_1:8;

then (A /\ B) \/ ({x} \/ B1) c= A \/ B by XBOOLE_1:4;

then A114: card ((A /\ B) \/ ({x} \/ B1)) c= card (A \/ B) by CARD_1:11;

assume not k + 2 c= card (A \/ B) ; :: thesis: contradiction

then A115: card (A \/ B) in succ (k + 1) by A5, ORDINAL1:16;

then A116: card (A \/ B) c= k + 1 by ORDINAL1:22;

( card (A \/ B) = k + 1 or ( card (A \/ B) in succ k & A c= A \/ B ) ) by A4, A115, ORDINAL1:8, XBOOLE_1:7;

then ( card (A \/ B) = k + 1 or ( card (A \/ B) c= k & k c= card (A \/ B) ) ) by A87, CARD_1:11, ORDINAL1:22;

then A117: ( card (A \/ B) = (k - 1) + (2 * 1) or card (A \/ B) = k + (2 * 0) ) by XBOOLE_0:def 10;

card A = (k - 1) + 1 by A87;

then A118: ( card (A /\ B) = k1 or card (A /\ B) = k ) by A101, A104, A117, Th2;

card ({x} \/ B1) = 2 + 1 by A95, A96, A98, CARD_2:41;

then ( card ((A /\ B) \/ ({x} \/ B1)) = (k - 1) + 3 or card ((A /\ B) \/ ({x} \/ B1)) = k + 3 ) by A95, A110, A118, CARD_2:40;

then ( Segm (k + 2) c= Segm (k + 1) or Segm (k + 3) c= Segm (k + 1) ) by A116, A114;

then ( k + 1 in k + 1 or k + 3 <= k + 1 ) by A5, NAT_1:39, ORDINAL1:21;

hence contradiction by XREAL_1:6; :: thesis: verum

proof

B in K
by A78, A101, A103, A106, A104;
assume
ex L being LINE of (G_ (k,X)) st {A2,B} on L
; :: thesis: contradiction

then consider L being LINE of (G_ (k,X)) such that

A120: {A2,B} on L ;

B on L by A120, INCSP_1:1;

then A121: B c= L by A1, A6, Th10;

L in the Lines of (G_ (k,X)) ;

then A122: ex L1 being Subset of X st

( L = L1 & card L1 = k + 1 ) by A8;

A2 on L by A120, INCSP_1:1;

then A c= L by A1, A6, A86, Th10;

then A \/ B c= L by A121, XBOOLE_1:8;

then A123: card (A \/ B) c= k + 1 by A122, CARD_1:11;

k + 2 c= k + 1 by A109, A123;

then k + 1 in k + 1 by A5, ORDINAL1:21;

hence contradiction ; :: thesis: verum

end;then consider L being LINE of (G_ (k,X)) such that

A120: {A2,B} on L ;

B on L by A120, INCSP_1:1;

then A121: B c= L by A1, A6, Th10;

L in the Lines of (G_ (k,X)) ;

then A122: ex L1 being Subset of X st

( L = L1 & card L1 = k + 1 ) by A8;

A2 on L by A120, INCSP_1:1;

then A c= L by A1, A6, A86, Th10;

then A \/ B c= L by A121, XBOOLE_1:8;

then A123: card (A \/ B) c= k + 1 by A122, CARD_1:11;

k + 2 c= k + 1 by A109, A123;

then k + 1 in k + 1 by A5, ORDINAL1:21;

hence contradiction ; :: thesis: verum

hence contradiction by A81, A82, A84, A86, A119; :: thesis: verum

proof

hence
K is maximal_clique
by A79; :: thesis: verum
let A, B be POINT of (G_ (k,X)); :: according to COMBGRAS:def 2 :: thesis: ( A in K & B in K implies ex L being LINE of (G_ (k,X)) st {A,B} on L )

assume that

A124: A in K and

A125: B in K ; :: thesis: ex L being LINE of (G_ (k,X)) st {A,B} on L

S in the Lines of (G_ (k,X)) by A8, A77;

then consider L being LINE of (G_ (k,X)) such that

A126: L = S ;

ex B1 being Subset of X st

( B1 = B & card B1 = k & B1 c= S ) by A78, A125;

then A127: B on L by A1, A6, A126, Th10;

ex A1 being Subset of X st

( A1 = A & card A1 = k & A1 c= S ) by A78, A124;

then A on L by A1, A6, A126, Th10;

then {A,B} on L by A127, INCSP_1:1;

hence ex L being LINE of (G_ (k,X)) st {A,B} on L ; :: thesis: verum

end;assume that

A124: A in K and

A125: B in K ; :: thesis: ex L being LINE of (G_ (k,X)) st {A,B} on L

S in the Lines of (G_ (k,X)) by A8, A77;

then consider L being LINE of (G_ (k,X)) such that

A126: L = S ;

ex B1 being Subset of X st

( B1 = B & card B1 = k & B1 c= S ) by A78, A125;

then A127: B on L by A1, A6, A126, Th10;

ex A1 being Subset of X st

( A1 = A & card A1 = k & A1 c= S ) by A78, A124;

then A on L by A1, A6, A126, Th10;

then {A,B} on L by A127, INCSP_1:1;

hence ex L being LINE of (G_ (k,X)) st {A,B} on L ; :: thesis: verum