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 ;
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 ;
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 ;
A9: succ (Segm k1) = Segm (k1 + 1) by NAT_1:38;
A10: ( K is STAR implies K is maximal_clique )
proof
assume K is STAR ; :: thesis:
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 ;
A14: for U being Subset of the Points of (G_ (k,X)) st U is clique & K c= U holds
U = K
proof
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 ;
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 ;
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 ;
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 ;
then A25: card (S /\ A) c= k - 2 by ;
A26: not X \ (A \/ S) <> {}
proof
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 ;
then A30: not y in S by XBOOLE_0:def 3;
then A31: card (S \/ {y}) = (k - 1) + 1 by ;
A32: {y} c= X by ;
then S \/ {y} c= X by XBOOLE_1:8;
then S \/ {y} in the Points of (G_ (k,X)) by ;
then consider B being POINT of (G_ (k,X)) such that
A33: B = S \/ {y} ;
A34: not y in A by ;
A /\ B c= A /\ S
proof
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 ;
then A36: ( a in S or a in {y} ) by XBOOLE_0:def 3;
a in A by ;
hence a in A /\ S by ; :: thesis: verum
end;
then card (A /\ B) c= card (A /\ S) by CARD_1:11;
then card (A /\ B) c= k - 2 by A25;
then A37: card (A /\ B) in k - 1 by ;
A38: for L being LINE of (G_ (k,X)) holds not {A2,B} on L
proof
A <> B by ;
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 ;
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 ;
then A c= L by A1, A6, A21, Th10;
then A \/ B c= L by ;
then card (A \/ B) c= k + 1 by ;
then A43: card (A \/ B) = (k - 1) + (2 * 1) by ;
card B = (k - 1) + 1 by ;
then card (A /\ B) = k1 by ;
hence contradiction by A37; :: thesis: verum
end;
A44: S c= B by ;
B c= X by ;
then B in K by A12, A31, A33, A44;
hence contradiction by A16, A17, A19, A21, A38; :: thesis: verum
end;
k1 < k1 + 1 by NAT_1:13;
then card S in Segm k by ;
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 ;
then A46: card (S \/ {x}) = (k - 1) + 1 by ;
A47: {x} c= A by ;
x in A by A45;
then A48: {x} c= X by ;
then A49: S \/ {x} c= X by XBOOLE_1:8;
not X \ (A \/ S) = {}
proof
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 ;
then A52: A \/ B = A \/ S by ;
A \/ S c= X by ;
then A53: A \/ S = X by ;
A54: 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: contradiction
then consider L being LINE of (G_ (k,X)) such that
A55: {A2,B} on L ;
B on L by ;
then A56: B c= L by A1, A6, Th10;
A2 on L by ;
then A c= L by A1, A6, A21, Th10;
then A \/ B c= L by ;
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 ;
hence contradiction ; :: thesis: verum
end;
( S c= B & B c= X ) by ;
then B in K by ;
hence contradiction by A16, A17, A19, A21, A54; :: thesis: verum
end;
hence contradiction by A26; :: thesis: verum
end;
K is clique
proof
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 ;
then A61: A is finite ;
A62: ex B1 being Subset of X st
( B1 = B & card B1 = k & S c= B1 ) by ;
then S c= A /\ B by ;
then k - 1 c= card (A /\ B) by ;
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 ;
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
A66: card A <> card X
proof
assume card A = card X ; :: thesis: contradiction
then k in k by ;
hence contradiction ; :: thesis: verum
end;
card A c= card X by ;
then card A in card X by ;
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 ;
then A68: A \/ {x} c= X by ;
not x in A by ;
then card (A \/ {x}) = k + 1 by ;
then A \/ {x} in the Lines of (G_ (k,X)) by ;
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 ;
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 ;
hence ex L being LINE of (G_ (k,X)) st {A,B} on L ; :: thesis: verum
end;
A71: ( card (A /\ B) = k - 1 implies ex L being LINE of (G_ (k,X)) st {A,B} on L )
proof
A72: A \/ B c= X by ;
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 ;
then A \/ B in the Lines of (G_ (k,X)) by ;
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 ;
hence ex L being LINE of (G_ (k,X)) st {A,B} on L ; :: thesis: verum
end;
card (A /\ B) c= k by ;
hence ex L being LINE of (G_ (k,X)) st {A,B} on L by ; :: thesis: verum
end;
hence K is maximal_clique by A14; :: thesis: verum
end;
A76: succ 0 = 0 + 1 ;
( K is TOP implies K is maximal_clique )
proof
assume K is TOP ; :: thesis:
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
A80: k - 2 <= (k - 2) + 1 by ;
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 ;
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 ;
A89: not A c= S by ;
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 ;
then card A in card S by ;
then A92: S \ A <> {} by CARD_1:68;
2 c= card (S \ A)
proof
A93: not card (S \ A) = 1
proof
assume card (S \ A) = 1 ; :: thesis: contradiction
then A94: card (S \ (S \ A)) = (k + 1) - 1 by ;
( S \ (S \ A) = S /\ A & S /\ A c= S ) by ;
hence contradiction by A87, A89, A94, CARD_2:102, XBOOLE_1:17; :: thesis: verum
end;
assume not 2 c= card (S \ A) ; :: thesis: contradiction
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 ;
hence contradiction by A92, A93; :: thesis: verum
end;
then consider B1 being set such that
A95: B1 c= S \ A and
A96: card B1 = 2 by CARD_FIL:36;
A97: B1 c= S by ;
then A98: not x in B1 by A91;
card (S \ B1) = (k + 1) - 2 by ;
then Segm k2 c= Segm (card (S \ B1)) by ;
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 ;
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 ;
then B1 \/ B2 in the Points of (G_ (k,X)) by ;
then consider B being POINT of (G_ (k,X)) such that
A104: B = B1 \/ B2 ;
B1 misses A by ;
then A105: B1 /\ A = {} by XBOOLE_0:def 7;
B2 c= S by ;
then A106: B1 \/ B2 c= S by ;
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
A110: {x} \/ B1 misses A /\ B
proof
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 ;
then A112: ( y in A & y in B ) by XBOOLE_0:def 4;
y in {x} \/ B1 by ;
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;
{x} c= A by ;
then {x} c= A \/ B by XBOOLE_1:10;
then A113: (A /\ B) \/ {x} c= A \/ B by ;
B1 c= B by ;
then B1 c= A \/ B by XBOOLE_1:10;
then ((A /\ B) \/ {x}) \/ B1 c= A \/ B by ;
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 ;
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 ;
then ( card (A \/ B) = k + 1 or ( card (A \/ B) c= k & k c= card (A \/ B) ) ) by ;
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 ;
card ({x} \/ B1) = 2 + 1 by ;
then ( card ((A /\ B) \/ ({x} \/ B1)) = (k - 1) + 3 or card ((A /\ B) \/ ({x} \/ B1)) = k + 3 ) by ;
then ( Segm (k + 2) c= Segm (k + 1) or Segm (k + 3) c= Segm (k + 1) ) by ;
then ( k + 1 in k + 1 or k + 3 <= k + 1 ) by ;
hence contradiction by XREAL_1:6; :: thesis: verum
end;
A119: 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: contradiction
then consider L being LINE of (G_ (k,X)) such that
A120: {A2,B} on L ;
B on L by ;
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 ;
then A c= L by A1, A6, A86, Th10;
then A \/ B c= L by ;
then A123: card (A \/ B) c= k + 1 by ;
k + 2 c= k + 1 by ;
then k + 1 in k + 1 by ;
hence contradiction ; :: thesis: verum
end;
B in K by ;
hence contradiction by A81, A82, A84, A86, A119; :: thesis: verum
end;
K is clique
proof
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 ;
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 ;
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 ;
then A on L by A1, A6, A126, Th10;
then {A,B} on L by ;
hence ex L being LINE of (G_ (k,X)) st {A,B} on L ; :: thesis: verum
end;
hence K is maximal_clique by A79; :: thesis: verum
end;
hence ( ( K is STAR or K is TOP ) implies K is maximal_clique ) by A10; :: thesis: verum