let k be Element of NAT ; :: thesis:
let X be non empty set ; :: thesis:
assume A1: ( 2 <= k & k + 2 c= card X ) ; :: thesis:
then A2: ( k - 2 is Element of NAT & k + 1 <= k + 2 & 1 <= k ) by NAT_1:21, XREAL_1:9, XXREAL_0:2;
then ( - 2 < 0 & k + 1 c= k + 2 ) by NAT_1:40;
then A3: ( 2 - 2 < k & k + 1 c= card X ) by A1, XBOOLE_1:1;
A4: k - 1 is Element of NAT by A2, NAT_1:21;
A5: the Points of (G_ k,X) = { A where A is Subset of X : card A = k } by A3, Def1;
A6: the Lines of (G_ k,X) = { L where L is Subset of X : card L = k + 1 } by A3, Def1;
let K be Subset of the Points of (G_ k,X); :: thesis:
A7: ( succ (k - 1) = (k - 1) + 1 & succ k = k + 1 & succ (k + 1) = (k + 1) + 1 & card k = k & card (k - 1) = k - 1 & card 2 = 2 & card 1 = 1 & card 0 = 0 & succ 1 = 1 + 1 & succ 0 = 0 + 1 & card (k + 1) = k + 1 & card (k - 2) = k - 2 & succ (k - 2) = (k - 2) + 1 & succ 2 = 2 + 1 ) by A2, A4, CARD_1:def 5, NAT_1:39;
A8: ( K is STAR implies K is maximal_clique )

proof

assume K is STAR ; :: thesis:
then consider S being Subset of X such that
A9: ( card S = k - 1 & K = { A where A is Subset of X : ( card A = k & S c= A ) } ) by Def4;
A10: S is finite by A4, A9;
A11: K is clique

proof

let A, B be POINT of (G_ k,X); :: according to COMBGRAS:def 2 :: thesis:
assume A12: ( A in K & B in K ) ; :: thesis:
then consider A1 being Subset of X such that
A13: ( A1 = A & card A1 = k & S c= A1 ) by A9;
consider B1 being Subset of X such that
A14: ( B1 = B & card B1 = k & S c= B1 ) by A9, A12;
A15: ( A is finite & B is finite & A /\ B c= A & A /\ B c= B ) by A13, A14, XBOOLE_1:17;
S c= A /\ B by A13, A14, XBOOLE_1:19;
then A17: ( k - 1 c= card (A /\ B) & card (A /\ B) c= k ) by A9, A13, A15, CARD_1:27;
then k - 1 in succ (card (A /\ B)) by A4, ORDINAL1:34;
then ( card (A /\ B) = k - 1 or k - 1 in card (A /\ B) ) by ORDINAL1:13;
then A18: ( card (A /\ B) = k - 1 or k c= card (A /\ B) ) by A7, ORDINAL1:33;
A19: ( card (A /\ B) = k - 1 implies ex L being LINE of (G_ k,X) st {A,B} on L )

proof

assume A20: card (A /\ B) = k - 1 ; :: thesis:
( card A = (k - 1) + 1 & card B = (k - 1) + 1 ) by A13, A14;
then ( card (A \/ B) = (k - 1) + (2 * 1) & A \/ B c= X ) by A4, A13, A14, A20, Th2, XBOOLE_1:8;
then A \/ B in the Lines of (G_ k,X) by A6;
then consider L being LINE of (G_ k,X) such that
A21: L = A \/ B ;
( A c= A \/ B & B c= A \/ B ) by XBOOLE_1:7;
then ( A on L & B on L ) by A3, A21, Th10;
then {A,B} on L by INCSP_1:11;
hence ex L being LINE of (G_ k,X) st {A,B} on L ; :: thesis:

end;

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

proof

assume card (A /\ B) = k ; :: thesis:
then A22: ( A /\ B = A & A /\ B = B ) by A13, A14, A15, CARD_FIN:1;
A23: card A c= card X by A13, CARD_1:27;
card A <> card X

proof

assume card A = card X ; :: thesis:
then k in k by A3, A7, A13, ORDINAL1:33;
hence contradiction ; :: thesis:

end;

then card A in card X by A23, CARD_1:13;
then X \ A <> {} by CARD_2:4;
then consider x being set such that
A24: x in X \ A by XBOOLE_0:def 1;
( x in X & not x in A ) by A24, XBOOLE_0:def 5;
then A25: ( card (A \/ {x}) = k + 1 & {x} c= X ) by A13, A15, CARD_2:54, ZFMISC_1:37;
then A \/ {x} c= X by A13, XBOOLE_1:8;
then A \/ {x} in the Lines of (G_ k,X) by A6, A25;
then consider L being LINE of (G_ k,X) such that
A26: L = A \/ {x} ;
( A c= A \/ {x} & B c= A \/ {x} ) by A22, XBOOLE_1:7;
then ( A on L & B on L ) by A3, A26, Th10;
then {A,B} on L by INCSP_1:11;
hence ex L being LINE of (G_ k,X) st {A,B} on L ; :: thesis:

end;

hence ex L being LINE of (G_ k,X) st {A,B} on L by A17, A18, A19, XBOOLE_0:def 10; :: thesis:

end;

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

proof

let U be Subset of the Points of (G_ k,X); :: thesis:
assume A27: ( U is clique & K c= U & U <> K ) ; :: thesis:
then not U c= K by XBOOLE_0:def 10;
then consider A being set such that
A28: ( A in U & not A in K ) by TARSKI:def 3;
A29: A in the Points of (G_ k,X) by A28;
consider A2 being POINT of (G_ k,X) such that
A30: A2 = A by A28;
consider A1 being Subset of X such that
A31: ( A1 = A & card A1 = k ) by A5, A29;
A32: ( not S c= A & A is finite & A c= X ) by A9, A28, A31;
A33: ( S /\ A c= S & S /\ A c= A ) by XBOOLE_1:17;
card (S /\ A) c= k - 1 by A9, CARD_1:27, XBOOLE_1:17;
then ( card (S /\ A) in succ (k - 1) & succ (k - 2) = (k - 2) + 1 ) by A2, A4, NAT_1:39, ORDINAL1:34;
then ( card (S /\ A) in succ (k - 2) or card (S /\ A) = k - 1 ) by ORDINAL1:13;
then A35: card (S /\ A) c= k - 2 by A2, A9, A10, A32, A33, CARD_FIN:1, ORDINAL1:34;
k - 1 < (k - 1) + 1 by A4, NAT_1:13;
then card S in card A by A4, A9, A31, NAT_1:45;
then A \ S <> {} by CARD_2:4;
then consider x being set such that
A36: x in A \ S by XBOOLE_0:def 1;
( x in A & not x in S ) by A36, XBOOLE_0:def 5;
then A37: ( card (S \/ {x}) = (k - 1) + 1 & x in X & {x} c= A & {x} c= X ) by A9, A10, A31, CARD_2:54, ZFMISC_1:37;
then A38: S \/ {x} c= X by XBOOLE_1:8;
A39: not X \ (A \/ S) = {}

proof

assume X \ (A \/ S) = {} ; :: thesis:
then ( X c= A \/ S & A \/ S c= X ) by A31, XBOOLE_1:8, XBOOLE_1:37;
then A40: ( X \ A c= S & A \/ S = X ) by XBOOLE_0:def 10, XBOOLE_1:43;
S \/ {x} in the Points of (G_ k,X) by A5, A37, A38;
then consider B being POINT of (G_ k,X) such that
A41: B = S \/ {x} ;
( A \/ B = (A \/ S) \/ {x} & S c= B & {x} c= A \/ S & B c= X ) by A37, A41, XBOOLE_1:4, XBOOLE_1:8, XBOOLE_1:10;
then A42: ( B in K & A \/ B = A \/ S ) by A9, A37, A41, XBOOLE_1:12;
for L being LINE of (G_ k,X) holds not {A2,B} on L

proof

assume ex L being LINE of (G_ k,X) st {A2,B} on L ; :: thesis:
then consider L being LINE of (G_ k,X) such that
A43: {A2,B} on L ;
L in the Lines of (G_ k,X) ;
then consider L1 being Subset of X such that
A44: ( L = L1 & card L1 = k + 1 ) by A6;
( A2 on L & B on L ) by A43, INCSP_1:11;
then ( A c= L & B c= L ) by A3, A30, Th10;
then A \/ B c= L by XBOOLE_1:8;
then card (A \/ B) c= card L by CARD_1:27;
then k + 2 c= card L by A1, A40, A42, XBOOLE_1:1;
then k + 1 in k + 1 by A7, A44, ORDINAL1:33;
hence contradiction ; :: thesis:

end;

hence contradiction by A27, A28, A30, A42, Def2; :: thesis:

end;

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

proof

assume X \ (A \/ S) <> {} ; :: thesis:
then consider y being set such that
A45: y in X \ (A \/ S) by XBOOLE_0:def 1;
( y in X & not y in A \/ S ) by A45, XBOOLE_0:def 5;
then A46: ( not y in A & not y in S & {y} c= X ) by XBOOLE_0:def 3, ZFMISC_1:37;
then A47: ( card (S \/ {y}) = (k - 1) + 1 & S \/ {y} c= X ) by A9, A10, CARD_2:54, XBOOLE_1:8;
then S \/ {y} in the Points of (G_ k,X) by A5;
then consider B being POINT of (G_ k,X) such that
A48: B = S \/ {y} ;
( S c= B & B c= X ) by A46, A48, XBOOLE_1:7, XBOOLE_1:8;
then A49: B in K by A9, A47, A48;
A /\ B c= A /\ S

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in A /\ B ; :: thesis:
then A50: ( a in A & a in S \/ {y} ) by A48, XBOOLE_0:def 4;
then ( a in S or a in {y} ) by XBOOLE_0:def 3;
hence a in A /\ S by A46, A50, TARSKI:def 1, XBOOLE_0:def 4; :: thesis:

end;

then card (A /\ B) c= card (A /\ S) by CARD_1:27;
then ( card (A /\ B) c= k - 2 & succ (k - 2) = (k - 2) + 1 ) by A2, A35, NAT_1:39, XBOOLE_1:1;
then A51: card (A /\ B) in k - 1 by A2, ORDINAL1:34;
for L being LINE of (G_ k,X) holds not {A2,B} on L

proof

assume ex L being LINE of (G_ k,X) st {A2,B} on L ; :: thesis:
then consider L being LINE of (G_ k,X) such that
A52: {A2,B} on L ;
L in the Lines of (G_ k,X) ;
then consider L1 being Subset of X such that
A53: ( L = L1 & card L1 = k + 1 ) by A6;
( A2 on L & B on L ) by A52, INCSP_1:11;
then ( A c= L & B c= L ) by A3, A30, Th10;
then A54: A \/ B c= L by XBOOLE_1:8;
A <> B

proof

assume A = B ; :: thesis:
then {y} c= A by A48, XBOOLE_1:7;
hence contradiction by A46, ZFMISC_1:37; :: thesis:

end;

then ( k + 1 c= card (A \/ B) & card (A \/ B) c= k + 1 ) by A31, A47, A48, A53, A54, Th1, CARD_1:27;
then ( card (A \/ B) = (k - 1) + (2 * 1) & card A = (k - 1) + 1 & card B = (k - 1) + 1 ) by A9, A10, A31, A46, A48, CARD_2:54, XBOOLE_0:def 10;
then card (A /\ B) = k - 1 by A4, Th2;
hence contradiction by A51; :: thesis:

end;

hence contradiction by A27, A28, A30, A49, Def2; :: thesis:

end;

hence contradiction by A39; :: thesis:

end;

hence K is maximal_clique by A11, Def3; :: thesis:

end;

( K is TOP implies K is maximal_clique )

proof

assume K is TOP ; :: thesis:
then consider S being Subset of X such that
A55: ( card S = k + 1 & K = { A where A is Subset of X : ( card A = k & A c= S ) } ) by Def5;
A56: S is finite by A55;
A57: K is clique

proof

let A, B be POINT of (G_ k,X); :: according to COMBGRAS:def 2 :: thesis:
assume A58: ( A in K & B in K ) ; :: thesis:
then consider A1 being Subset of X such that
A59: ( A1 = A & card A1 = k & A1 c= S ) by A55;
consider B1 being Subset of X such that
A60: ( B1 = B & card B1 = k & B1 c= S ) by A55, A58;
S in the Lines of (G_ k,X) by A6, A55;
then consider L being LINE of (G_ k,X) such that
A61: L = S ;
( A on L & B on L ) by A3, A59, A60, A61, Th10;
then {A,B} on L by INCSP_1:11;
hence ex L being LINE of (G_ k,X) st {A,B} on L ; :: thesis:

end;

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

proof

let U be Subset of the Points of (G_ k,X); :: thesis:
assume A62: ( U is clique & K c= U & U <> K ) ; :: thesis:
then not U c= K by XBOOLE_0:def 10;
then consider A being set such that
A63: ( A in U & not A in K ) by TARSKI:def 3;
A64: A in the Points of (G_ k,X) by A63;
consider A2 being POINT of (G_ k,X) such that
A65: A2 = A by A63;
consider A1 being Subset of X such that
A66: ( A1 = A & card A1 = k ) by A5, A64;
A67: ( not A c= S & A is finite & A c= X ) by A55, A63, A66;
then consider x being set such that
A68: ( x in A & not x in S ) by TARSKI:def 3;
k <= k + 1 by NAT_1:11;
then A69: card A c= card S by A55, A66, NAT_1:40;
card A <> card S by A55, A66;
then card A in card S by A69, CARD_1:13;
then S \ A <> {} by CARD_2:4;
then A70: card (S \ A) <> 0 ;
2 c= card (S \ A)

proof

assume not 2 c= card (S \ A) ; :: thesis:
then ( card (S \ A) in succ 1 & 0 c= card (S \ A) ) by ORDINAL1:26;
then ( card (S \ A) in 1 or card (S \ A) = 1 ) by ORDINAL1:13;
then A72: ( card (S \ A) c= 0 or card (S \ A) = 1 ) by A7, ORDINAL1:34;
not card (S \ A) = 1

proof

assume A73: card (S \ A) = 1 ; :: thesis:
A74: S \ A c= S by XBOOLE_1:36;
A75: ( card (S \ (S \ A)) = (k + 1) - 1 & S \ (S \ A) = S /\ A & S /\ A c= S & S /\ A c= A ) by A55, A56, A73, A74, CARD_2:63, XBOOLE_1:17, XBOOLE_1:48;
thus contradiction by A66, A67, A75, CARD_FIN:1; :: thesis:

end;

hence contradiction by A70, A72; :: thesis:

end;

then consider B1 being set such that
A76: ( B1 c= S \ A & card B1 = 2 ) by CARD_FIL:36;
A77: ( B1 c= S & B1 misses A ) by A76, XBOOLE_1:106;
then A78: B1 is finite by A56;
A79: card (S \ B1) = (k + 1) - 2 by A55, A56, A76, A77, CARD_2:63;
k - 2 <= (k - 2) + 1 by A2, NAT_1:11;
then k - 2 c= card (S \ B1) by A2, A79, NAT_1:40;
then consider B2 being set such that
A80: ( B2 c= S \ B1 & card B2 = k - 2 ) by A2, CARD_FIL:36;
A81: ( B2 c= S & B2 misses B1 ) by A80, XBOOLE_1:106;
then ( B2 is finite & B1 c= X & B2 c= X ) by A56, A76, XBOOLE_1:1;
then A82: ( card (B1 \/ B2) = 2 + (k - 2) & B1 \/ B2 c= X & B1 \/ B2 c= S ) by A76, A77, A78, A80, A81, CARD_2:53, XBOOLE_1:8;
then B1 \/ B2 in the Points of (G_ k,X) by A5;
then consider B being POINT of (G_ k,X) such that
A83: B = B1 \/ B2 ;
A84: ( A /\ B c= A \/ B & not x in B1 & not x in B2 & A \/ B = A \/ (B1 \/ B2) & B c= S ) by A68, A77, A81, A83, XBOOLE_1:8, XBOOLE_1:29;
A85: ( not x in B1 \/ B2 & B1 /\ A = {} & (B1 /\ A) /\ B c= B1 /\ A & B in K ) by A55, A68, A77, A82, A83, XBOOLE_0:def 7, XBOOLE_1:17;
A86: k + 2 c= card (A \/ B)

proof

assume not k + 2 c= card (A \/ B) ; :: thesis:
then A87: card (A \/ B) in succ (k + 1) by A7, ORDINAL1:26;
A88: {x} \/ B1 misses A /\ B

proof

assume not {x} \/ B1 misses A /\ B ; :: thesis:
then ({x} \/ B1) /\ (A /\ B) <> {} by XBOOLE_0:def 7;
then consider y being set such that
A89: y in ({x} \/ B1) /\ (A /\ B) by XBOOLE_0:def 1;
( y in {x} \/ B1 & y in A /\ B ) by A89, XBOOLE_0:def 4;
then ( ( y in {x} or y in B1 ) & y in A & y in B ) by XBOOLE_0:def 3, XBOOLE_0:def 4;
hence contradiction by A83, A85, TARSKI:def 1, XBOOLE_0:def 4; :: thesis:

end;

( (B1 /\ A) /\ B c= {} & {x} c= A ) by A68, A85, ZFMISC_1:37;
then ( (B1 /\ A) /\ B = {} & B1 c= B & {x} c= A \/ B ) by A83, XBOOLE_1:10;
then ( B1 /\ (A /\ B) = {} & B1 c= A \/ B & (A /\ B) \/ {x} c= A \/ B ) by A84, XBOOLE_1:8, XBOOLE_1:10, XBOOLE_1:16;
then ((A /\ B) \/ {x}) \/ B1 c= A \/ B by XBOOLE_1:8;
then A90: ( (A /\ B) \/ ({x} \/ B1) c= A \/ B & card (A \/ B) c= k + 1 ) by A87, ORDINAL1:34, XBOOLE_1:4;
( card (A \/ B) = k + 1 or ( card (A \/ B) in succ k & A c= A \/ B ) ) by A7, A87, ORDINAL1:13, XBOOLE_1:7;
then ( card (A \/ B) = k + 1 or ( card (A \/ B) c= k & k c= card (A \/ B) ) ) by A66, CARD_1:27, ORDINAL1:34;
then ( ( card (A \/ B) = (k - 1) + (2 * 1) or card (A \/ B) = k + (2 * 0 ) ) & card A = k + 0 & card B = k + 0 & card A = (k - 1) + 1 & card B = (k - 1) + 1 ) by A66, A82, A83, XBOOLE_0:def 10;
then A91: ( card (A /\ B) = k - 1 or card (A /\ B) = k ) by A4, Th2;
( card ({x} \/ B1) = 2 + 1 & {x} \/ B1 is finite & A /\ B is finite ) by A67, A76, A78, A84, CARD_2:54;
then ( ( card ((A /\ B) \/ ({x} \/ B1)) = (k - 1) + 3 or card ((A /\ B) \/ ({x} \/ B1)) = k + 3 ) & card ((A /\ B) \/ ({x} \/ B1)) c= card (A \/ B) ) by A88, A90, A91, CARD_1:27, CARD_2:53;
then ( k + 2 c= k + 1 or k + 3 c= k + 1 ) by A90, XBOOLE_1:1;
then ( k + 1 in k + 1 or k + 3 <= k + 1 ) by A7, NAT_1:40, ORDINAL1:33;
hence contradiction by XREAL_1:8; :: thesis:

end;

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

proof

assume ex L being LINE of (G_ k,X) st {A2,B} on L ; :: thesis:
then consider L being LINE of (G_ k,X) such that
A92: {A2,B} on L ;
L in the Lines of (G_ k,X) ;
then consider L1 being Subset of X such that
A93: ( L = L1 & card L1 = k + 1 ) by A6;
( A2 on L & B on L ) by A92, INCSP_1:11;
then ( A c= L & B c= L ) by A3, A65, Th10;
then A \/ B c= L by XBOOLE_1:8;
then ( k + 1 c= card (A \/ B) & card (A \/ B) c= k + 1 ) by A66, A68, A82, A83, A85, A93, Th1, CARD_1:27;
then k + 2 c= k + 1 by A86, XBOOLE_0:def 10;
then k + 1 in k + 1 by A7, ORDINAL1:33;
hence contradiction ; :: thesis:

end;

hence contradiction by A62, A63, A65, A85, Def2; :: thesis:

end;

hence K is maximal_clique by A57, Def3; :: thesis:

end;

hence ( ( K is STAR or K is TOP ) implies K is maximal_clique ) by A8; :: thesis: