let R be RelStr ; :: thesis: ( R is with_finite_clique# & R is with_finite_stability# implies R is finite )
assume A1: R is with_finite_clique# ; :: thesis: ( not R is with_finite_stability# or R is finite )
assume A2: R is with_finite_stability# ; :: thesis: R is finite
assume A3: R is infinite ; :: thesis: contradiction
reconsider R = R as with_finite_clique# with_finite_stability# RelStr by A1, A2;
consider C being finite Clique of R such that
A4: card C = clique# R by Def4;
consider An being finite StableSet of R such that
A5: card An = stability# R by Def6;
set h = clique# R;
set w = stability# R;
A6: 0 + 1 <= clique# R by A3, NAT_1:13;
A7: 0 + 1 <= stability# R by A3, NAT_1:13;
set cR = the carrier of R;
A8: the carrier of R = [#] R ;
per cases ( clique# R = 1 or stability# R = 1 or ( clique# R > 1 & stability# R > 1 ) ) by A6, A7, XXREAL_0:1;
suppose clique# R = 1 ; :: thesis: contradiction
then A9: the carrier of R is StableSet of R by A8, Th19;
consider Y being finite Subset of the carrier of R such that
A10: card Y > stability# R by A3, Th5;
Y is StableSet of R by A9, Th16;
hence contradiction by A10, Def6; :: thesis: verum
end;
suppose stability# R = 1 ; :: thesis: contradiction
then A11: the carrier of R is Clique of R by A8, Th21;
consider Y being finite Subset of the carrier of R such that
A12: card Y > clique# R by A3, Th5;
Y is Clique of R by A11, Th9;
hence contradiction by A12, Def4; :: thesis: verum
end;
suppose A13: ( clique# R > 1 & stability# R > 1 ) ; :: thesis: contradiction
set m = (max ((clique# R),(stability# R))) + 1;
reconsider m = (max ((clique# R),(stability# R))) + 1 as Nat ;
consider r being Nat 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 R such that
A15: card Y > r by A3, Th5;
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 A16: card Y <= card X by NAT_1:43, 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 ) } };
A17: { {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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or x in the_subsets_of_card (2,X) )
reconsider x1 = x as set by TARSKI:1;
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: x in the_subsets_of_card (2,X)
then consider xx, yy being Element of R such that
A18: {xx,yy} = x and
A19: xx <> yy and
A20: xx in X and
A21: yy in X and
( xx <= yy or yy <= xx ) ;
( x is Subset of X & card x1 = 2 ) by A18, A19, A20, A21, CARD_2:57, ZFMISC_1:32;
hence x in the_subsets_of_card (2,X) ; :: thesis: verum
end;
A22: { {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 object ; :: according to TARSKI:def 3 :: thesis: ( not 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 ) } or x in the_subsets_of_card (2,X) )
reconsider x1 = x as set by TARSKI:1;
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: x in the_subsets_of_card (2,X)
then consider xx, yy being Element of R such that
A23: {xx,yy} = x and
A24: xx <> yy and
A25: xx in X and
A26: yy in X and
( not xx <= yy & not yy <= xx ) ;
( x is Subset of X & card x1 = 2 ) by A23, A24, A25, A26, CARD_2:57, ZFMISC_1:32;
hence x in the_subsets_of_card (2,X) ; :: thesis: verum
end;
A27: ( { {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;
A28: now :: thesis: not { {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 ) }
assume A29: { {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: contradiction
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 R by A30, A31;
A33: ( not a <= b & not b <= a ) by A30, A31, A32, Def2;
( 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 R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } by A33, A32;
then consider aa, bb being Element of R such that
A34: {a,b} = {aa,bb} and
( aa <> bb & aa in X & bb in X ) and
A35: ( aa <= bb or bb <= aa ) by A29;
( ( a = aa & b = bb ) or ( a = bb & b = aa ) ) by A34, ZFMISC_1:6;
hence contradiction by A35, A30, A31, A32, Def2; :: thesis: verum
end;
A36: { { {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 object ; :: according to TARSKI:def 3 :: thesis: ( not 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 ) } } or x in bool (the_subsets_of_card (2,X)) )
reconsider xx = x as set by TARSKI:1;
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: x in bool (the_subsets_of_card (2,X))
then xx c= the_subsets_of_card (2,X) by A17, A22, TARSKI:def 2;
hence x in bool (the_subsets_of_card (2,X)) ; :: thesis: verum
end;
A37: 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: 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 ) } }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not 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 ) } } or x in the_subsets_of_card (2,X) )
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: x in the_subsets_of_card (2,X)
then consider Y being set such that
A38: x in Y and
A39: 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 A39, TARSKI:def 2;
hence x in the_subsets_of_card (2,X) by A38, A17, A22; :: thesis: verum
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: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the_subsets_of_card (2,X) or 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 ) } } )
assume x in the_subsets_of_card (2,X) ; :: thesis: 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 ) } }
then consider xx being Subset of X such that
A40: x = xx and
A41: card xx = 2 ;
consider a, b being object 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 R ;
A44: ( a in xx & b in xx ) by A43, 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 A44, A42;
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 A40, A43, A27, TARSKI:def 4; :: thesis: verum
end;
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: ( 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 ) } } implies ( 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 ) ) ) )
assume A45: 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: ( 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 ) ) )
thus a <> {} :: thesis: 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
per cases ( 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 ) } ) by A45, TARSKI:def 2;
suppose A46: a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } ; :: thesis: a <> {}
consider aa, bb being set such that
A47: aa in C and
A48: bb in C and
A49: aa <> bb by A13, A4, NAT_1:59;
reconsider aa = aa, bb = bb as Element of R by A47, A48;
A50: ( aa <= bb or bb <= aa ) by A47, A48, A49, Th6;
( aa in (Y \/ An) \/ C & bb in (Y \/ An) \/ C ) by A47, A48, 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 A50, A49;
hence a <> {} by A46; :: thesis: verum
end;
suppose A51: 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: a <> {}
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 R by A52, A53;
A55: ( not aa <= bb & not bb <= aa ) by A52, A53, A54, Def2;
( 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 R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } by A55, A54;
hence a <> {} by A51; :: thesis: verum
end;
end;
end;
let b be Subset of (the_subsets_of_card (2,X)); :: thesis: ( 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 )
assume A56: 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: ( a = b or a misses b )
assume A57: a <> b ; :: thesis: a misses b
assume A58: a meets b ; :: thesis: contradiction
( ( 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 A45, A56, 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 A57, A58;
then consider x being object such that
A59: 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 A59, XBOOLE_0:def 4;
then consider xx, yy being Element of R such that
A60: {xx,yy} = x and
( xx <> yy & xx in X & yy in X ) and
A61: ( 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 A59, XBOOLE_0:def 4;
then consider x2, y2 being Element of R such that
A62: {x2,y2} = x and
( x2 <> y2 & x2 in X & y2 in X ) and
A63: ( not x2 <= y2 & not y2 <= x2 ) ;
( ( xx = x2 & yy = y2 ) or ( xx = y2 & yy = x2 ) ) by A60, A62, ZFMISC_1:6;
hence contradiction by A61, A63; :: thesis: verum
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 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 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 ( p = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or p = { {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;
suppose A69: p = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } ; :: thesis: contradiction
now :: thesis: for x, y being Element of R st x in S & y in S & x <> y & not x <= y holds
y <= x
let x, y be Element of R; :: thesis: ( x in S & y in S & x <> y & not x <= y implies y <= x )
assume that
A70: x in S and
A71: y in S and
A72: x <> y ; :: thesis: ( x <= y or y <= x )
( {x,y} is Subset of S & card {x,y} = 2 ) by 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 R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } by A69, A68;
then consider xx, yy being Element of R such that
A73: {xx,yy} = {x,y} and
( xx <> yy & xx in X & yy in X ) and
A74: ( xx <= yy or yy <= xx ) ;
( ( xx = x & yy = y ) or ( xx = y & yy = x ) ) by A73, ZFMISC_1:6;
hence ( x <= y or y <= x ) by A74; :: thesis: verum
end;
then S is Clique of R by Th6;
hence contradiction by A66, Def4; :: thesis: verum
end;
suppose A75: 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: contradiction
S is stable
proof
let x, y be Element of R; :: according to DILWORTH:def 2 :: thesis: ( x in S & y in S & x <> y implies ( not x <= y & not y <= x ) )
assume that
A76: x in S and
A77: y in S and
A78: x <> y ; :: thesis: ( not x <= y & not y <= x )
( {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 R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } by A75, A68;
then consider xx, yy being Element of R such that
A79: {xx,yy} = {x,y} and
( xx <> yy & xx in X & yy in X ) and
A80: ( not xx <= yy & not yy <= xx ) ;
( ( xx = x & yy = y ) or ( xx = y & yy = x ) ) by A79, ZFMISC_1:6;
hence ( not x <= y & not y <= x ) by A80; :: thesis: verum
end;
hence contradiction by A67, Def6; :: thesis: verum
end;
end;
end;
end;