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;
A4: Vertices R is infinite by A3, Th23;
A5: 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
A6: order C = clique# R by Def15;
reconsider VC = Vertices C as finite Subset of (Vertices R) by ZFMISC_1:77;
consider An being finite StableSet of R such that
A7: card An = stability# R by Def24;
reconsider VAn = An as finite Subset of (Vertices R) ;
set h = clique# R;
set w = stability# R;
A8: 0 + 1 <= clique# R by A4, Th54, NAT_1:14;
not R is void by A3;
then A9: 0 + 1 <= stability# R by NAT_1:13;

per cases by A8, A9, XXREAL_0:1;

suppose clique# R = 1 ; :: thesis:

then A10: Vertices R is StableSet of R by Th63;
consider Y being finite Subset of (Vertices R) such that
A11: card Y > stability# R by A4, DILWORTH:5;
Y is StableSet of R by A10, Th64;
hence contradiction by A11, Def24; :: thesis:

end;

suppose stability# R = 1 ; :: thesis:

then A12: R is Clique of R by A5, Th71;
consider Y being finite Subset of (Vertices R) such that
A13: card Y > clique# R by A4, DILWORTH:5;
A14: R SubgraphInducedBy Y is Clique of R by A12, Th66;
order (R SubgraphInducedBy Y) = card Y by Lm9;
hence contradiction by A13, A14, Def15; :: thesis:

end;

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

set m = (max ((clique# R),(stability# R))) + 1;
reconsider m = (max ((clique# R),(stability# R))) + 1 as Nat ;
consider r being Nat such that
A16: 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
A17: card Y > r by A4, 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 A18: 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 ) } };
A19: { {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 object ; :: according to TARSKI:def 3 :: thesis:
reconsider x1 = x as set by TARSKI:1;
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
A20: {xx,yy} = x and
A21: xx <> yy and
A22: xx in X and
A23: yy in X and
{xx,yy} in Edges R ;
( x is Subset of X & card x1 = 2 ) by A20, A21, A22, A23, CARD_2:57, ZFMISC_1:32;
hence x in the_subsets_of_card (2,X) ; :: thesis:

end;

A24: { {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 object ; :: according to TARSKI:def 3 :: thesis:
reconsider x1 = x as set by TARSKI:1;
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
A25: {xx,yy} = x and
A26: xx <> yy and
A27: xx in X and
A28: yy in X and
{xx,yy} nin Edges R ;
( x is Subset of X & card x1 = 2 ) by A25, A26, A27, A28, CARD_2:57, ZFMISC_1:32;
hence x in the_subsets_of_card (2,X) ; :: thesis:

end;

A29: ( { {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;

A30: now :: thesis:

assume A31: { {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
A32: a in An and
A33: b in An and
A34: a <> b by A15, A7, NAT_1:59;
reconsider a = a, b = b as Element of Vertices R by A32, A33;
A35: {a,b} nin Edges R by A32, A33, A34, Def19;
( a in Y \/ An & b in Y \/ An ) by A32, A33, 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 A35, A34;
then consider aa, bb being Element of Vertices R such that
A36: {a,b} = {aa,bb} and
( aa <> bb & aa in X & bb in X ) and
A37: {aa,bb} in Edges R by A31;
thus contradiction by A37, A32, A33, A34, Def19, A36; :: thesis:

end;

A38: { { {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 object ; :: according to TARSKI:def 3 :: thesis:
reconsider x1 = x as set by TARSKI:1;
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 x1 c= the_subsets_of_card (2,X) by A19, A24, TARSKI:def 2;
hence x in bool (the_subsets_of_card (2,X)) ; :: thesis:

end;

A39: 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 object ; :: 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
A40: x in Y and
A41: 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 A41, TARSKI:def 2;
hence x in the_subsets_of_card (2,X) by A40, A19, A24; :: 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 object ; :: 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
A42: x = xx and
A43: card xx = 2 ;
consider a, b being object such that
A44: a <> b and
A45: xx = {a,b} by A43, CARD_2:60;
( a in xx & b in xx ) by A45, TARSKI:def 2;
then ( a in X & b in X ) ;
then reconsider a = a, b = b as Element of Vertices R ;
A46: ( a in xx & b in xx ) by A45, 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 A46, A44;
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 A42, A45, A29, 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 A47: 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 A47, TARSKI:def 2;

suppose A48: 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
A49: aa in VC and
A50: bb in VC and
A51: aa <> bb by A15, A6, NAT_1:59;
reconsider aa = aa, bb = bb as Element of Vertices R by A49, A50;
{aa,bb} in C by A49, A50, Th53;
then A52: {aa,bb} in Edges R by A51, Th12;
( aa in (Y \/ An) \/ VC & bb in (Y \/ An) \/ VC ) by A49, A50, 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 A51, A52;
hence a <> {} by A48; :: thesis:

end;

suppose A53: 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
A54: aa in An and
A55: bb in An and
A56: aa <> bb by A15, A7, NAT_1:59;
reconsider aa = aa, bb = bb as Element of Vertices R by A54, A55;
A57: {aa,bb} nin Edges R by A54, A55, A56, Def19;
( aa in Y \/ An & bb in Y \/ An ) by A54, A55, 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 A56, A57;
hence a <> {} by A53; :: thesis:

end;

let b be Subset of (the_subsets_of_card (2,X)); :: thesis:
assume A58: 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 A59: a <> b ; :: thesis:
assume A60: 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 A47, A58, 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 A59, A60;
then consider x being object such that
A61: 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 A61, XBOOLE_0:def 4;
then consider xx, yy being Element of Vertices R such that
A62: {xx,yy} = x and
( xx <> yy & xx in X & yy in X ) and
A63: {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 A61, XBOOLE_0:def 4;
then consider x2, y2 being Element of Vertices R such that
A64: {x2,y2} = x and
( x2 <> y2 & x2 in X & y2 in X ) and
A65: {x2,y2} nin Edges R ;
thus contradiction by A63, A65, A62, A64; :: 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 A39, A38, EQREL_1:def 4;
card P = 2 by A30, CARD_2:57;
then consider S being Subset of X such that
A66: card S >= m and
A67: S is_homogeneous_for P by A18, A16, A17, 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 A68: card S > clique# R by A66, XXREAL_0:2;
max ((clique# R),(stability# R)) >= stability# R by XXREAL_0:25;
then m > stability# R by NAT_1:13;
then A69: card S > stability# R by A66, XXREAL_0:2;
consider p being Element of P such that
A70: the_subsets_of_card (2,S) c= p by A67, RAMSEY_1:def 1;

per cases by TARSKI:def 2;

suppose A71: 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;
A72: Vertices (R SubgraphInducedBy S) = S by Lm9;

now :: thesis:

let x, y be set ; :: thesis:
assume that
A73: x <> y and
A74: x in union (R SubgraphInducedBy S) and
A75: y in union (R SubgraphInducedBy S) ; :: thesis:
( {x,y} is Subset of S & card {x,y} = 2 ) by A72, A74, A75, A73, 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 A71, A70;
then consider xx, yy being Element of Vertices R such that
A76: {xx,yy} = {x,y} and
( xx <> yy & xx in X & yy in X ) and
A77: {xx,yy} in Edges R ;
{x,y} in R SubgraphInducedBy S by A77, A74, A75, A72, Lm10, A76;
hence {x,y} in Edges (R SubgraphInducedBy S) by A73, Th12; :: thesis:

end;

then R SubgraphInducedBy S is finite Clique of R by Th47;
then order (R SubgraphInducedBy S) <= clique# R by Def15;
hence contradiction by A68, Lm9; :: thesis:

end;

suppose A78: 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
A79: x <> y and
A80: x in S and
A81: y in S ; :: thesis:
( {x,y} is Subset of S & card {x,y} = 2 ) by A80, A81, A79, 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 A78, A70;
then consider xx, yy being Element of Vertices R such that
A82: {xx,yy} = {x,y} and
( xx <> yy & xx in X & yy in X ) and
A83: {xx,yy} nin Edges R ;
thus {x,y} nin R by A79, A83, Th12, A82; :: thesis:

end;

then S is stable ;
hence contradiction by A69, Def24; :: thesis:

end;