let R be non empty transitive antisymmetric with_finite_stability# RelStr ; :: thesis:
let A be StableSet of R; :: thesis:
let U be Clique-partition of (subrelstr (Upper A)); :: thesis:
let L be Clique-partition of (subrelstr (Lower A)); :: thesis:
assume that
A1: card A = stability# R and
A2: card U = stability# R and
A3: card L = stability# R ; :: thesis:
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 ; :: according to TARSKI:def 3 :: thesis:
reconsider xx = x as set by TARSKI:1;
assume x in rng (f .\/ g) ; :: thesis:
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 ; :: thesis:

end;

A21: union (rng (f .\/ g)) = the carrier of R

proof

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in union (rng (f .\/ g)) ; :: thesis:
then consider Y being set such that
A22: x in Y and
A23: Y in rng (f .\/ g) by TARSKI:def 4;
consider a being object such that
A24: a in dom (f .\/ g) and
A25: Y = (f .\/ g) . a by A23, FUNCT_1:def 3;
A26: x in (f . a) \/ (g . a) by A24, A25, A22, A15, LEXBFS:def 2;

per cases by A26, XBOOLE_0:def 3;

suppose A27: x in f . a ; :: thesis:

f . a in U by A24, A15, FUNCT_2:5;
then x in Upper A by A27, A5;
hence x in the carrier of R ; :: thesis:

end;

suppose A28: x in g . a ; :: thesis:

g . a in L by A24, A15, FUNCT_2:5;
then x in Lower A by A28, A6;
hence x in the carrier of R ; :: thesis:

end;

assume x in [#] R ; :: thesis:
then A29: x in (Upper A) \/ (Lower A) by A1, Th23;

per cases by A29, XBOOLE_0:def 3;

suppose x in Upper A ; :: thesis:

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; :: thesis:

end;

suppose x in Lower A ; :: thesis:

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; :: thesis:

end;

hence union (rng (f .\/ g)) = the carrier of R by TARSKI:2; :: thesis:

end;

A40: now :: thesis:

let a be Subset of the carrier of R; :: thesis:
assume a in rng (f .\/ g) ; :: thesis:
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; :: thesis:
let b be Subset of the carrier of R; :: thesis:
assume b in rng (f .\/ g) ; :: thesis:
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 ; :: thesis:
then 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 ; :: thesis:
then 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 by A55, A56, A42, A47, A43, A48, XBOOLE_0:def 3;

suppose ( z in cfx & z in cfy ) ; :: thesis:

then z in cfx /\ cfy by XBOOLE_0:def 4;
then cfx meets cfy ;
hence contradiction by A44, A49, A52, EQREL_1:def 4; :: thesis:

end;

suppose A57: ( z in cfx & z in cgy ) ; :: thesis:

then 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; :: thesis:

end;

suppose A64: ( z in cgx & z in cfy ) ; :: thesis:

then 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; :: thesis:

end;

suppose ( z in cgx & z in cgy ) ; :: thesis:

then z in cgx /\ cgy by XBOOLE_0:def 4;
then cgx meets cgy ;
hence contradiction by A45, A50, A53, EQREL_1:def 4; :: thesis:

end;

A71: for x being set st x in rng (f .\/ g) holds
x is Clique of R

proof

let c be set ; :: thesis:
assume c in rng (f .\/ g) ; :: thesis:
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 :: thesis:

let a, b be Element of R; :: thesis:
assume that
A79: a in c9 and
A80: b in c9 and
A81: a <> b ; :: thesis:
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 by A79, A80, A74, XBOOLE_0:def 3;

suppose ( a in f . x & b in f . x ) ; :: thesis:

hence ( a <= b or b <= a ) by A76, A81, Th6; :: thesis:

end;

suppose A84: ( a in f . x & b in g . x ) ; :: thesis:

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; :: thesis:

end;

suppose A86: ( a in g . x & b in f . x ) ; :: thesis:

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; :: thesis:

end;

suppose ( a in g . x & b in g . x ) ; :: thesis:

hence ( a <= b or b <= a ) by A78, A81, Th6; :: thesis:

end;

hence c is Clique of R by Th6; :: thesis:

end;

A88: f .\/ g is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A89: x1 in dom (f .\/ g) and
A90: x2 in dom (f .\/ g) and
A91: (f .\/ g) . x1 = (f .\/ g) . x2 ; :: thesis:
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; :: thesis:

end;

reconsider C = rng (f .\/ g) as Clique-partition of R by A16, A21, A40, A71, Def11, EQREL_1:def 4;
take C ; :: thesis:
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; :: thesis: