let R be SimpleGraph; :: thesis:
assume A1: R is with_finite_clique# ; :: thesis:
assume A2: R is with_finite_stability# ; :: thesis:
assume A3: R is infinite ; :: thesis:
set VR = Vertices R;
A3a: Vertices R is infinite by A3, FinSG;
A3bb: R c= R ;
reconsider R = R as with_finite_clique# with_finite_stability# SimpleGraph by A1, A2;
consider C being finite Clique of R such that
A4: order C = clique# R by Lcliqueno;
reconsider VC = Vertices C as finite Subset of (Vertices R) by ZFMISC_1:77;
consider An being finite StableSet of R such that
A5: card An = stability# R by Lstabno;
reconsider VAn = An as finite Subset of (Vertices R) ;
set h = clique# R;
set w = stability# R;
A6: 0 + 1 <= clique# R by A3a, Cno0, NAT_1:14;
not R is void by A3;
then A7: 0 + 1 <= stability# R by NAT_1:13;

per cases by A6, A7, XXREAL_0:1;

suppose clique# R = 1 ; :: thesis:

then A9: Vertices R is StableSet of R by Th19;
consider Y being finite Subset of (Vertices R) such that
A10: card Y > stability# R by A3a, DILWORTH:5;
Y is StableSet of R by A9, Th16;
hence contradiction by A10, Lstabno; :: thesis:

end;

suppose stability# R = 1 ; :: thesis:

then A11: R is Clique of R by A3bb, Th21;
consider Y being finite Subset of (Vertices R) such that
A12: card Y > clique# R by A3a, DILWORTH:5;
A12a: R SubgraphInducedBy Y is Clique of R by A11, SGClique0;
order (R SubgraphInducedBy Y) = card Y by Sub0c;
hence contradiction by A12, A12a, Lcliqueno; :: thesis:

end;

suppose A13: ( clique# R > 1 & stability# R > 1 ) ; :: thesis:

set m = (max ((clique# R),(stability# R))) + 1;
reconsider m = (max ((clique# R),(stability# R))) + 1 as natural number ;
consider r being natural number such that
A14: for X being finite set
for P being a_partition of the_subsets_of_card (2,X) st card X >= r & card P = 2 holds
ex S being Subset of X st
( card S >= m & S is_homogeneous_for P ) by RAMSEY_1:17;
consider Y being finite Subset of (Vertices R) such that
A15: card Y > r by A3a, DILWORTH:5;
set X = (Y \/ VAn) \/ VC;
reconsider X = (Y \/ VAn) \/ VC as finite Subset of (Vertices R) ;
( Y c= Y \/ An & Y \/ An c= (Y \/ An) \/ VC ) by XBOOLE_1:7;
then A16: card Y <= card X by NAT_1:43, XBOOLE_1:1;
set A = { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } ;
set B = { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } ;
set E = the_subsets_of_card (2,X);
set P = { { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } , { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } };
A17: { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } c= the_subsets_of_card (2,X)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } ; :: thesis:
then consider xx, yy being Element of Vertices R such that
A18: {xx,yy} = x and
A19: xx <> yy and
A20: xx in X and
A21: yy in X and
{xx,yy} in Edges R ;
( x is Subset of X & card x = 2 ) by A18, A19, A20, A21, CARD_2:57, ZFMISC_1:32;
hence x in the_subsets_of_card (2,X) ; :: thesis:

end;

A22: { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } c= the_subsets_of_card (2,X)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } ; :: thesis:
then consider xx, yy being Element of Vertices R such that
A23: {xx,yy} = x and
A24: xx <> yy and
A25: xx in X and
A26: yy in X and
{xx,yy} nin Edges R ;
( x is Subset of X & card x = 2 ) by A23, A24, A25, A26, CARD_2:57, ZFMISC_1:32;
hence x in the_subsets_of_card (2,X) ; :: thesis:

end;

A27: ( { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } in { { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } , { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } } & { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } in { { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } , { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } } ) by TARSKI:def 2;

A28: now :: thesis:

assume A29: { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } = { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } ; :: thesis:
consider a, b being set such that
A30: a in An and
A31: b in An and
A32: a <> b by A13, A5, NAT_1:59;
reconsider a = a, b = b as Element of Vertices R by A30, A31;
A33: {a,b} nin Edges R by A30, A31, A32, Lstable;
( a in Y \/ An & b in Y \/ An ) by A30, A31, XBOOLE_0:def 3;
then ( a in X & b in X ) by XBOOLE_0:def 3;
then {a,b} in { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } by A33, A32;
then consider aa, bb being Element of Vertices R such that
A34: {a,b} = {aa,bb} and
( aa <> bb & aa in X & bb in X ) and
A35: {aa,bb} in Edges R by A29;
thus contradiction by A35, A30, A31, A32, Lstable, A34; :: thesis:

end;

A36: { { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } , { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } } c= bool (the_subsets_of_card (2,X))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } , { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } } ; :: thesis:
then x c= the_subsets_of_card (2,X) by A17, A22, TARSKI:def 2;
hence x in bool (the_subsets_of_card (2,X)) ; :: thesis:

end;

A37: union { { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } , { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } } = the_subsets_of_card (2,X)

proof

thus union { { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } , { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } } c= the_subsets_of_card (2,X) :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in union { { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } , { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } } ; :: thesis:
then consider Y being set such that
A38: x in Y and
A39: Y in { { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } , { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } } by TARSKI:def 4;
( Y = { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } or Y = { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } ) by A39, TARSKI:def 2;
hence x in the_subsets_of_card (2,X) by A38, A17, A22; :: thesis:

end;

thus the_subsets_of_card (2,X) c= union { { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } , { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } } :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in the_subsets_of_card (2,X) ; :: thesis:
then consider xx being Subset of X such that
A40: x = xx and
A41: card xx = 2 ;
consider a, b being set such that
A42: a <> b and
A43: xx = {a,b} by A41, CARD_2:60;
( a in xx & b in xx ) by A43, TARSKI:def 2;
then ( a in X & b in X ) ;
then reconsider a = a, b = b as Element of Vertices R ;
A44: ( a in xx & b in xx ) by A43, TARSKI:def 2;
( {a,b} in Edges R or {a,b} nin Edges R ) ;
then ( {a,b} in { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } or {a,b} in { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } ) by A44, A42;
hence x in union { { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } , { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } } by A40, A43, A27, TARSKI:def 4; :: thesis:

end;

for a being Subset of (the_subsets_of_card (2,X)) st a in { { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } , { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } } holds
( a <> {} & ( for b being Subset of (the_subsets_of_card (2,X)) holds
( not b in { { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } , { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } } or a = b or a misses b ) ) )

proof

let a be Subset of (the_subsets_of_card (2,X)); :: thesis:
assume A45: a in { { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } , { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } } ; :: thesis:
thus a <> {} :: thesis:

proof

per cases by A45, TARSKI:def 2;

suppose A46: a = { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } ; :: thesis:

consider aa, bb being set such that
A47: aa in VC and
A48: bb in VC and
A49: aa <> bb by A13, A4, NAT_1:59;
reconsider aa = aa, bb = bb as Element of Vertices R by A47, A48;
{aa,bb} in C by A47, A48, Clique2a;
then A51: {aa,bb} in Edges R by A49, SG4a;
( aa in (Y \/ An) \/ VC & bb in (Y \/ An) \/ VC ) by A47, A48, XBOOLE_0:def 3;
then {aa,bb} in { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } by A49, A51;
hence a <> {} by A46; :: thesis:

end;

suppose A51: a = { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } ; :: thesis:

consider aa, bb being set such that
A52: aa in An and
A53: bb in An and
A54: aa <> bb by A13, A5, NAT_1:59;
reconsider aa = aa, bb = bb as Element of Vertices R by A52, A53;
A55a: {aa,bb} nin Edges R by A52, A53, A54, Lstable;
( aa in Y \/ An & bb in Y \/ An ) by A52, A53, XBOOLE_0:def 3;
then ( aa in X & bb in X ) by XBOOLE_0:def 3;
then {aa,bb} in { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } by A54, A55a;
hence a <> {} by A51; :: thesis:

end;

let b be Subset of (the_subsets_of_card (2,X)); :: thesis:
assume A56: b in { { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } , { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } } ; :: thesis:
assume A57: a <> b ; :: thesis:
assume A58: a meets b ; :: thesis:
( ( a = { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } or a = { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } ) & ( b = { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } or b = { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } ) ) by A45, A56, TARSKI:def 2;
then { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } /\ { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } <> {} by A57, A58, XBOOLE_0:def 7;
then consider x being set such that
A59: x in { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } /\ { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } by XBOOLE_0:def 1;
x in { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } by A59, XBOOLE_0:def 4;
then consider xx, yy being Element of Vertices R such that
A60: {xx,yy} = x and
( xx <> yy & xx in X & yy in X ) and
A61: {xx,yy} in Edges R ;
x in { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } by A59, XBOOLE_0:def 4;
then consider x2, y2 being Element of Vertices R such that
A62: {x2,y2} = x and
( x2 <> y2 & x2 in X & y2 in X ) and
A63: {x2,y2} nin Edges R ;
thus contradiction by A61, A63, A60, A62; :: thesis:

end;

then reconsider P = { { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } , { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } } as a_partition of the_subsets_of_card (2,X) by A37, A36, EQREL_1:def 4;
card P = 2 by A28, CARD_2:57;
then consider S being Subset of X such that
A64: card S >= m and
A65: S is_homogeneous_for P by A16, A14, A15, XXREAL_0:2;
reconsider S = S as finite Subset of (Vertices R) by XBOOLE_1:1;
max ((clique# R),(stability# R)) >= clique# R by XXREAL_0:25;
then m > clique# R by NAT_1:13;
then A66: card S > clique# R by A64, XXREAL_0:2;
max ((clique# R),(stability# R)) >= stability# R by XXREAL_0:25;
then m > stability# R by NAT_1:13;
then A67: card S > stability# R by A64, XXREAL_0:2;
consider p being Element of P such that
A68: the_subsets_of_card (2,S) c= p by A65, RAMSEY_1:def 1;

per cases by TARSKI:def 2;

suppose A69: p = { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } ; :: thesis:

set H = R SubgraphInducedBy S;
B72: Vertices (R SubgraphInducedBy S) = S by Sub0c;

now :: thesis:

let x, y be set ; :: thesis:
assume that
A72: x <> y and
A70: x in union (R SubgraphInducedBy S) and
A71: y in union (R SubgraphInducedBy S) ; :: thesis:
( {x,y} is Subset of S & card {x,y} = 2 ) by B72, A70, A71, A72, CARD_2:57, ZFMISC_1:32;
then {x,y} in the_subsets_of_card (2,S) ;
then {x,y} in { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} in Edges R ) } by A69, A68;
then consider xx, yy being Element of Vertices R such that
A73: {xx,yy} = {x,y} and
( xx <> yy & xx in X & yy in X ) and
A74: {xx,yy} in Edges R ;
{x,y} in R SubgraphInducedBy S by A74, A70, A71, B72, Sub6, A73;
hence {x,y} in Edges (R SubgraphInducedBy S) by A72, SG4a; :: thesis:

end;

then R SubgraphInducedBy S is finite Clique of R by Lclique1;
then order (R SubgraphInducedBy S) <= clique# R by Lcliqueno;
hence contradiction by A66, Sub0c; :: thesis:

end;

suppose A75: p = { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } ; :: thesis:

now :: thesis:

let x, y be set ; :: thesis:
assume that
A78: x <> y and
A76: x in S and
A77: y in S ; :: thesis:
( {x,y} is Subset of S & card {x,y} = 2 ) by A76, A77, A78, CARD_2:57, ZFMISC_1:32;
then {x,y} in the_subsets_of_card (2,S) ;
then {x,y} in { {x,y} where x, y is Element of Vertices R : ( x <> y & x in X & y in X & {x,y} nin Edges R ) } by A75, A68;
then consider xx, yy being Element of Vertices R such that
A79: {xx,yy} = {x,y} and
( xx <> yy & xx in X & yy in X ) and
A80: {xx,yy} nin Edges R ;
thus {x,y} nin R by A78, A80, SG4a, A79; :: thesis:

end;

then S is stable by Lstable;
hence contradiction by A67, Lstabno; :: thesis:

end;