let R be RelStr ; :: thesis:
assume A: R is with_finite_clique# ; :: thesis:
assume B: R is with_finite_stability# ; :: thesis:
assume C: not R is finite ; :: thesis:
reconsider R = R as with_finite_clique# with_finite_stability# RelStr by A, B;
consider C being finite Clique of R such that
D: card C = clique# R by Lheight;
consider An being finite StableSet of R such that
E: card An = stability# R by Lwidth;
set h = clique# R;
set w = stability# R;
hh: 0 + 1 <= clique# R by C, NAT_1:13;
ww: 0 + 1 <= stability# R by C, NAT_1:13;
set cR = the carrier of R;
cR: the carrier of R = [#] R ;

per cases by hh, ww, XXREAL_0:1;

suppose clique# R = 1 ; :: thesis:

then A1: the carrier of R is StableSet of R by cR, Height4;
consider Y being finite Subset of the carrier of R such that
B1: card Y > stability# R by C, Sinfset;
Y is StableSet of R by A1, AChain0;
hence contradiction by B1, Lwidth; :: thesis:

end;

suppose stability# R = 1 ; :: thesis:

then A1: the carrier of R is Clique of R by cR, Width4;
consider Y being finite Subset of the carrier of R such that
B1: card Y > clique# R by C, Sinfset;
Y is Clique of R by A1, Clique37;
hence contradiction by B1, Lheight; :: thesis:

end;

suppose S1: ( 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
G: 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 R such that
HY: card Y > r by C, Sinfset;
set X = (Y \/ An) \/ C;
reconsider X = (Y \/ An) \/ C as finite Subset of R ;
( Y c= Y \/ An & Y \/ An c= (Y \/ An) \/ C ) by XBOOLE_1:7;
then H1a: card Y <= card X by NAT_1:44, XBOOLE_1:1;
set A = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } ;
set B = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ;
set E = the_subsets_of_card (2,X);
set P = { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } };
As: { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } 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 R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } ; :: thesis:
then consider xx, yy being Element of R such that
D1: {xx,yy} = x and
E1: xx <> yy and
F1: xx in X and
G1: yy in X and
( xx <= yy or yy <= xx ) ;
( x is Subset of X & card x = 2 ) by D1, E1, F1, G1, ZFMISC_1:38, CARD_2:76;
hence x in the_subsets_of_card (2,X) ; :: thesis:

end;

Bs: { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } 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 R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ; :: thesis:
then consider xx, yy being Element of R such that
D1: {xx,yy} = x and
E1: xx <> yy and
F1: xx in X and
G1: yy in X and
( not xx <= yy & not yy <= xx ) ;
( x is Subset of X & card x = 2 ) by D1, E1, F1, G1, ZFMISC_1:38, CARD_2:76;
hence x in the_subsets_of_card (2,X) ; :: thesis:

end;

AB: ( { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } & { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } ) by TARSKI:def 2;

Ha: now

assume A2: { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ; :: thesis:
consider a, b being set such that
B2: a in An and
C2: b in An and
D2: a <> b by S1, E, GLIB_002:1;
reconsider a = a, b = b as Element of R by B2, C2;
E2: ( not a <= b & not b <= a ) by B2, C2, D2, LAChain;
( a in Y \/ An & b in Y \/ An ) by B2, C2, 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 R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } by E2, D2;
then consider aa, bb being Element of R such that
F2: {a,b} = {aa,bb} and
( aa <> bb & aa in X & bb in X ) and
H2: ( aa <= bb or bb <= aa ) by A2;
( ( a = aa & b = bb ) or ( a = bb & b = aa ) ) by F2, ZFMISC_1:10;
hence contradiction by H2, B2, C2, D2, LAChain; :: thesis:

end;

Hca: { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } 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 R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } ; :: thesis:
then x c= the_subsets_of_card (2,X) by As, Bs, TARSKI:def 2;
hence x in bool (the_subsets_of_card (2,X)) ; :: thesis:

end;

Hb: union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } = the_subsets_of_card (2,X)

proof

thus union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } 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 R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } ; :: thesis:
then consider Y being set such that
A3: x in Y and
B3: Y in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } by TARSKI:def 4;
( Y = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or Y = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ) by B3, TARSKI:def 2;
hence x in the_subsets_of_card (2,X) by A3, As, Bs; :: thesis:

end;

thus the_subsets_of_card (2,X) c= union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } :: 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
A2: x = xx and
B2: card xx = 2 ;
consider a, b being set such that
C2: a <> b and
D2: xx = {a,b} by B2, CARD_2:79;
( a in xx & b in xx ) by D2, TARSKI:def 2;
then ( a in X & b in X ) ;
then reconsider a = a, b = b as Element of R ;
E2a: ( a in xx & b in xx ) by D2, TARSKI:def 2;
( ( not a <= b & not b <= a ) or a <= b or b <= a ) ;
then ( {a,b} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or {a,b} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ) by E2a, C2;
hence x in union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } by A2, D2, AB, 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 R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } 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 R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or a = b or a misses b ) ) )

proof

let a be Subset of (the_subsets_of_card (2,X)); :: thesis:
assume A2: a in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } ; :: thesis:
thus a <> {} :: thesis:

proof

per cases by A2, TARSKI:def 2;

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

consider aa, bb being set such that
B3: aa in C and
C3: bb in C and
D3: aa <> bb by S1, D, GLIB_002:1;
reconsider aa = aa, bb = bb as Element of R by B3, C3;
E3: ( aa <= bb or bb <= aa ) by B3, C3, D3, DClique;
( aa in (Y \/ An) \/ C & bb in (Y \/ An) \/ C ) by B3, C3, XBOOLE_0:def 3;
then {aa,bb} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } by E3, D3;
hence a <> {} by S2; :: thesis:

end;

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

consider aa, bb being set such that
B3: aa in An and
C3: bb in An and
D3: aa <> bb by S1, E, GLIB_002:1;
reconsider aa = aa, bb = bb as Element of R by B3, C3;
E3: ( not aa <= bb & not bb <= aa ) by B3, C3, D3, LAChain;
( aa in Y \/ An & bb in Y \/ An ) by B3, C3, 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 R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } by E3, D3;
hence a <> {} by S2; :: thesis:

end;

let b be Subset of (the_subsets_of_card (2,X)); :: thesis:
assume B2: b in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } ; :: thesis:
assume C2: a <> b ; :: thesis:
assume D2: a meets b ; :: thesis:
( ( a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ) & ( b = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or b = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ) ) by A2, B2, TARSKI:def 2;
then { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } /\ { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } <> {} by C2, D2, XBOOLE_0:def 7;
then consider x being set such that
E2: x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } /\ { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } by XBOOLE_0:def 1;
x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } by E2, XBOOLE_0:def 4;
then consider xx, yy being Element of R such that
F1: {xx,yy} = x and
( xx <> yy & xx in X & yy in X ) and
G1: ( xx <= yy or yy <= xx ) ;
x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } by E2, XBOOLE_0:def 4;
then consider x2, y2 being Element of R such that
H1: {x2,y2} = x and
( x2 <> y2 & x2 in X & y2 in X ) and
I1: ( not x2 <= y2 & not y2 <= x2 ) ;
( ( xx = x2 & yy = y2 ) or ( xx = y2 & yy = x2 ) ) by F1, H1, ZFMISC_1:10;
hence contradiction by G1, I1; :: thesis:

end;

then reconsider P = { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } as a_partition of the_subsets_of_card (2,X) by Hb, Hca, EQREL_1:def 6;
card P = 2 by Ha, CARD_2:76;
then consider S being Subset of X such that
K: card S >= m and
L: S is_homogeneous_for P by H1a, G, HY, XXREAL_0:2;
reconsider S = S as finite Subset of 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 mh: card S > clique# R by K, XXREAL_0:2;
max ((clique# R),(stability# R)) >= stability# R by XXREAL_0:25;
then m > stability# R by NAT_1:13;
then mw: card S > stability# R by K, XXREAL_0:2;
consider p being Element of P such that
M: the_subsets_of_card (2,S) c= p by L, RAMSEY_1:def 1;

per cases by TARSKI:def 2;

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

now

let x, y be Element of R; :: thesis:
assume that
A1: x in S and
B1: y in S and
C1: x <> y ; :: thesis:
( {x,y} is Subset of S & card {x,y} = 2 ) by A1, B1, C1, ZFMISC_1:38, CARD_2:76;
then {x,y} in the_subsets_of_card (2,S) ;
then {x,y} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } by S1, M;
then consider xx, yy being Element of R such that
D1: {xx,yy} = {x,y} and
( xx <> yy & xx in X & yy in X ) and
E1: ( xx <= yy or yy <= xx ) ;
( ( xx = x & yy = y ) or ( xx = y & yy = x ) ) by D1, ZFMISC_1:10;
hence ( x <= y or y <= x ) by E1; :: thesis:

end;

then S is Clique of R by DClique;
hence contradiction by mh, Lheight; :: thesis:

end;

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

S is stable

proof

let x, y be Element of R; :: according to DILWORTH:def 2 :: thesis:
assume that
A1: x in S and
B1: y in S and
C1: x <> y ; :: thesis:
( {x,y} is Subset of S & card {x,y} = 2 ) by A1, B1, C1, ZFMISC_1:38, CARD_2:76;
then {x,y} in the_subsets_of_card (2,S) ;
then {x,y} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } by S1, M;
then consider xx, yy being Element of R such that
D1: {xx,yy} = {x,y} and
( xx <> yy & xx in X & yy in X ) and
E1: ( not xx <= yy & not yy <= xx ) ;
( ( xx = x & yy = y ) or ( xx = y & yy = x ) ) by D1, ZFMISC_1:10;
hence ( not x <= y & not y <= x ) by E1; :: thesis:

end;

hence contradiction by mw, Lwidth; :: thesis:

end;