let R be non empty transitive antisymmetric with_finite_stability# RelStr ; for A being StableSet of R
for U being Clique-partition of (subrelstr (Upper A))
for L being Clique-partition of (subrelstr (Lower A)) st card A = stability# R & card U = stability# R & card L = stability# R holds
ex C being Clique-partition of R st card C = stability# R
let A be StableSet of R; for U being Clique-partition of (subrelstr (Upper A))
for L being Clique-partition of (subrelstr (Lower A)) st card A = stability# R & card U = stability# R & card L = stability# R holds
ex C being Clique-partition of R st card C = stability# R
let U be Clique-partition of (subrelstr (Upper A)); for L being Clique-partition of (subrelstr (Lower A)) st card A = stability# R & card U = stability# R & card L = stability# R holds
ex C being Clique-partition of R st card C = stability# R
let L be Clique-partition of (subrelstr (Lower A)); ( card A = stability# R & card U = stability# R & card L = stability# R implies ex C being Clique-partition of R st card C = stability# R )
assume that
A1:
card A = stability# R
and
A2:
card U = stability# R
and
A3:
card L = stability# R
; ex C being Clique-partition of R st card C = stability# R
A4:
not A is empty
by A1;
set aA = Upper A;
set bA = Lower A;
set cR = the carrier of R;
set Pa = subrelstr (Upper A);
set Pb = subrelstr (Lower A);
A5:
Upper A = the carrier of (subrelstr (Upper A))
by YELLOW_0:def 15;
A6:
Lower A = the carrier of (subrelstr (Lower A))
by YELLOW_0:def 15;
reconsider Pa = subrelstr (Upper A) as non empty transitive antisymmetric with_finite_stability# RelStr by A4;
A /\ (Upper A) = A
by XBOOLE_1:21;
then
A is StableSet of Pa
by Th31;
then consider f being Function of A,U such that
A7:
f is bijective
and
A8:
for x being set st x in A holds
x in f . x
by A1, A2, Th47;
A9:
dom f = A
by A4, FUNCT_2:def 1;
A10:
rng f = U
by A7, FUNCT_2:def 3;
reconsider Pb = subrelstr (Lower A) as non empty transitive antisymmetric with_finite_stability# RelStr by A4;
A /\ (Lower A) = A
by XBOOLE_1:21;
then
A is StableSet of Pb
by Th31;
then consider g being Function of A,L such that
A11:
g is bijective
and
A12:
for x being set st x in A holds
x in g . x
by A1, A3, Th47;
A13:
dom g = A
by A4, FUNCT_2:def 1;
A14:
rng g = L
by A11, FUNCT_2:def 3;
set h = f .\/ g;
set C = rng (f .\/ g);
A15:
dom (f .\/ g) = (dom f) \/ (dom g)
by LEXBFS:def 2;
A16:
rng (f .\/ g) c= bool the carrier of R
proof
let x be
object ;
TARSKI:def 3 ( not x in rng (f .\/ g) or x in bool the carrier of R )
reconsider xx =
x as
set by TARSKI:1;
assume
x in rng (f .\/ g)
;
x in bool the carrier of R
then consider a being
object such that A17:
a in dom (f .\/ g)
and A18:
(f .\/ g) . a = x
by FUNCT_1:def 3;
A19:
(f .\/ g) . a = (f . a) \/ (g . a)
by A17, A15, LEXBFS:def 2;
f . a in U
by A17, A15, FUNCT_2:5;
then A20:
f . a c= the
carrier of
R
by A5, XBOOLE_1:1;
g . a in L
by A17, A15, FUNCT_2:5;
then
g . a c= the
carrier of
R
by A6, XBOOLE_1:1;
then
xx c= the
carrier of
R
by A18, A19, A20, XBOOLE_1:8;
hence
x in bool the
carrier of
R
;
verum
end;
A21:
union (rng (f .\/ g)) = the carrier of R
proof
now for x being object holds
( ( x in union (rng (f .\/ g)) implies x in the carrier of R ) & ( x in [#] R implies x in union (rng (f .\/ g)) ) )let x be
object ;
( ( x in union (rng (f .\/ g)) implies x in the carrier of R ) & ( x in [#] R implies b1 in union (rng (f .\/ g)) ) )assume
x in [#] R
;
b1 in union (rng (f .\/ g))then A29:
x in (Upper A) \/ (Lower A)
by A1, Th23;
per cases
( x in Upper A or x in Lower A )
by A29, XBOOLE_0:def 3;
suppose
x in Upper A
;
b1 in union (rng (f .\/ g))then
x in union U
by A5, EQREL_1:def 4;
then consider Y being
set such that A30:
x in Y
and A31:
Y in U
by TARSKI:def 4;
consider a being
object such that A32:
a in dom f
and A33:
Y = f . a
by A31, A10, FUNCT_1:def 3;
A34:
(f .\/ g) . a in rng (f .\/ g)
by A32, A15, A9, A13, FUNCT_1:3;
(f .\/ g) . a = (f . a) \/ (g . a)
by A32, A15, A9, A13, LEXBFS:def 2;
then
x in (f .\/ g) . a
by A30, A33, XBOOLE_0:def 3;
hence
x in union (rng (f .\/ g))
by A34, TARSKI:def 4;
verum end; suppose
x in Lower A
;
b1 in union (rng (f .\/ g))then
x in union L
by A6, EQREL_1:def 4;
then consider Y being
set such that A35:
x in Y
and A36:
Y in L
by TARSKI:def 4;
consider a being
object such that A37:
a in dom g
and A38:
Y = g . a
by A36, A14, FUNCT_1:def 3;
A39:
(f .\/ g) . a in rng (f .\/ g)
by A37, A15, A9, A13, FUNCT_1:3;
(f .\/ g) . a = (f . a) \/ (g . a)
by A37, A15, A9, A13, LEXBFS:def 2;
then
x in (f .\/ g) . a
by A35, A38, XBOOLE_0:def 3;
hence
x in union (rng (f .\/ g))
by A39, TARSKI:def 4;
verum end; end; end;
hence
union (rng (f .\/ g)) = the
carrier of
R
by TARSKI:2;
verum
end;
A40:
now for a being Subset of the carrier of R st a in rng (f .\/ g) holds
( a <> {} & ( for b being Subset of the carrier of R st b in rng (f .\/ g) & a <> b holds
not a meets b ) )let a be
Subset of the
carrier of
R;
( a in rng (f .\/ g) implies ( a <> {} & ( for b being Subset of the carrier of R st b in rng (f .\/ g) & a <> b holds
not a meets b ) ) )assume
a in rng (f .\/ g)
;
( a <> {} & ( for b being Subset of the carrier of R st b in rng (f .\/ g) & a <> b holds
not a meets b ) )then consider x being
object such that A41:
x in dom (f .\/ g)
and A42:
(f .\/ g) . x = a
by FUNCT_1:def 3;
A43:
(f .\/ g) . x = (f . x) \/ (g . x)
by A41, A15, LEXBFS:def 2;
set cfx =
f . x;
set cgx =
g . x;
A44:
f . x in U
by A41, A15, FUNCT_2:5;
then reconsider cfx =
f . x as
Subset of
Pa ;
A45:
g . x in L
by A41, A15, FUNCT_2:5;
then reconsider cgx =
g . x as
Subset of
Pb ;
cfx <> {}
by A44;
hence
a <> {}
by A42, A43;
for b being Subset of the carrier of R st b in rng (f .\/ g) & a <> b holds
not a meets blet b be
Subset of the
carrier of
R;
( b in rng (f .\/ g) & a <> b implies not a meets b )assume
b in rng (f .\/ g)
;
( a <> b implies not a meets b )then consider y being
object such that A46:
y in dom (f .\/ g)
and A47:
(f .\/ g) . y = b
by FUNCT_1:def 3;
A48:
(f .\/ g) . y = (f . y) \/ (g . y)
by A46, A15, LEXBFS:def 2;
set cfy =
f . y;
set cgy =
g . y;
A49:
f . y in U
by A46, A15, FUNCT_2:5;
then reconsider cfy =
f . y as
Subset of
Pa ;
A50:
g . y in L
by A46, A15, FUNCT_2:5;
then reconsider cgy =
g . y as
Subset of
Pb ;
assume A51:
a <> b
;
not a meets bthen A52:
cfx <> cfy
by A7, A42, A47, A41, A46, A15, A9, FUNCT_1:def 4;
A53:
cgx <> cgy
by A11, A51, A42, A47, A41, A46, A15, A13, FUNCT_1:def 4;
assume
a meets b
;
contradictionthen
a /\ b <> {}
;
then consider z being
object such that A54:
z in a /\ b
by XBOOLE_0:def 1;
A55:
z in a
by A54, XBOOLE_0:def 4;
A56:
z in b
by A54, XBOOLE_0:def 4;
set cfz =
f . z;
set cgz =
g . z;
per cases
( ( z in cfx & z in cfy ) or ( z in cfx & z in cgy ) or ( z in cgx & z in cfy ) or ( z in cgx & z in cgy ) )
by A55, A56, A42, A47, A43, A48, XBOOLE_0:def 3;
suppose A57:
(
z in cfx &
z in cgy )
;
contradictionthen A58:
z in A
by A5, A6, Th22;
A59:
z in f . z
by A57, A5, A6, Th22, A8;
A60:
f . z in U
by A57, A5, A6, Th22, FUNCT_2:5;
then reconsider cfz =
f . z as
Subset of
Pa ;
z in cfx /\ cfz
by A57, A59, XBOOLE_0:def 4;
then
cfz meets cfx
;
then
cfz = cfx
by A44, A60, EQREL_1:def 4;
then A61:
z = x
by A7, A41, A58, A15, A9, FUNCT_1:def 4;
A62:
z in g . z
by A57, A5, A6, Th22, A12;
A63:
g . z in L
by A57, A5, A6, Th22, FUNCT_2:5;
then reconsider cgz =
g . z as
Subset of
Pb ;
z in cgz /\ cgy
by A57, A62, XBOOLE_0:def 4;
then
cgz meets cgy
;
then
cgz = cgy
by A50, A63, EQREL_1:def 4;
hence
contradiction
by A61, A51, A42, A47, A11, A46, A58, A15, A13, FUNCT_1:def 4;
verum end; suppose A64:
(
z in cgx &
z in cfy )
;
contradictionthen A65:
z in A
by A5, A6, Th22;
A66:
z in f . z
by A64, A5, A6, Th22, A8;
A67:
f . z in U
by A64, A5, A6, Th22, FUNCT_2:5;
then reconsider cfz =
f . z as
Subset of
Pa ;
z in cfy /\ cfz
by A64, A66, XBOOLE_0:def 4;
then
cfz meets cfy
;
then
cfz = cfy
by A49, A67, EQREL_1:def 4;
then A68:
z = y
by A7, A46, A65, A15, A9, FUNCT_1:def 4;
A69:
z in g . z
by A64, A5, A6, Th22, A12;
A70:
g . z in L
by A64, A5, A6, Th22, FUNCT_2:5;
then reconsider cgz =
g . z as
Subset of
Pb ;
z in cgz /\ cgx
by A64, A69, XBOOLE_0:def 4;
then
cgz meets cgx
;
then
cgz = cgx
by A45, A70, EQREL_1:def 4;
hence
contradiction
by A68, A51, A42, A47, A11, A41, A65, A15, A13, FUNCT_1:def 4;
verum end; end; end;
A71:
for x being set st x in rng (f .\/ g) holds
x is Clique of R
proof
let c be
set ;
( c in rng (f .\/ g) implies c is Clique of R )
assume
c in rng (f .\/ g)
;
c is Clique of R
then consider x being
object such that A72:
x in dom (f .\/ g)
and A73:
c = (f .\/ g) . x
by FUNCT_1:def 3;
A74:
c = (f . x) \/ (g . x)
by A72, A73, A15, LEXBFS:def 2;
set cf =
f . x;
set cg =
g . x;
f . x in U
by A72, A15, FUNCT_2:5;
then A75:
f . x is
Clique of
Pa
by Def11;
then A76:
f . x is
Clique of
R
by Th28;
g . x in L
by A72, A15, FUNCT_2:5;
then A77:
g . x is
Clique of
Pb
by Def11;
then A78:
g . x is
Clique of
R
by Th28;
then reconsider c9 =
c as
Subset of
R by A74, A76, XBOOLE_1:8;
now for a, b being Element of R st a in c9 & b in c9 & a <> b & not a <= b holds
b <= alet a,
b be
Element of
R;
( a in c9 & b in c9 & a <> b & not b1 <= b2 implies b2 <= b1 )assume that A79:
a in c9
and A80:
b in c9
and A81:
a <> b
;
( b1 <= b2 or b2 <= b1 )A82:
x in f . x
by A72, A15, A8;
A83:
x in g . x
by A72, A15, A12;
reconsider x =
x as
Element of
R by A72, A15, A9, A13;
per cases
( ( a in f . x & b in f . x ) or ( a in f . x & b in g . x ) or ( a in g . x & b in f . x ) or ( a in g . x & b in g . x ) )
by A79, A80, A74, XBOOLE_0:def 3;
suppose A84:
(
a in f . x &
b in g . x )
;
( b1 <= b2 or b2 <= b1 )then A85:
(
x = a or
x <= a )
by A82, A72, A15, A75, Th35;
(
x = b or
b <= x )
by A83, A84, A72, A15, A77, Th34;
hence
(
a <= b or
b <= a )
by A81, A85, YELLOW_0:def 2;
verum end; suppose A86:
(
a in g . x &
b in f . x )
;
( b1 <= b2 or b2 <= b1 )then A87:
(
x = a or
a <= x )
by A83, A72, A15, A77, Th34;
(
x = b or
x <= b )
by A82, A86, A72, A15, A75, Th35;
hence
(
a <= b or
b <= a )
by A81, A87, YELLOW_0:def 2;
verum end; end; end;
hence
c is
Clique of
R
by Th6;
verum
end;
A88:
f .\/ g is one-to-one
proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in dom (f .\/ g) or not x2 in dom (f .\/ g) or not (f .\/ g) . x1 = (f .\/ g) . x2 or x1 = x2 )
assume that A89:
x1 in dom (f .\/ g)
and A90:
x2 in dom (f .\/ g)
and A91:
(f .\/ g) . x1 = (f .\/ g) . x2
;
x1 = x2
A92:
(f .\/ g) . x1 is
Clique of
R
by A71, A89, FUNCT_1:3;
A93:
(f .\/ g) . x1 = (f . x1) \/ (g . x1)
by A15, A89, LEXBFS:def 2;
(
x1 in f . x1 &
x1 in g . x1 )
by A89, A15, A8, A12;
then A94:
x1 in (f .\/ g) . x1
by A93, XBOOLE_0:def 3;
A95:
(f .\/ g) . x2 = (f . x2) \/ (g . x2)
by A15, A90, LEXBFS:def 2;
(
x2 in f . x2 &
x2 in g . x2 )
by A90, A15, A8, A12;
then
x2 in (f .\/ g) . x2
by A95, XBOOLE_0:def 3;
hence
x1 = x2
by A15, A89, A90, A91, A92, A94, Th15;
verum
end;
reconsider C = rng (f .\/ g) as Clique-partition of R by A16, A21, A40, A71, Def11, EQREL_1:def 4;
take
C
; card C = stability# R
card C =
card (f .\/ g)
by A88, PRE_POLY:19
.=
card A
by A15, A9, A13, CARD_1:62
;
hence
card C = stability# R
by A1; verum