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
B1: card U = stability# R and
C1: card L = stability# R ; :: thesis:
D1: 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);
S2d: Upper A = the carrier of (subrelstr (Upper A)) by YELLOW_0:def 15;
S2e: 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 D1;
A /\ (Upper A) = A by XBOOLE_1:21;
then A is StableSet of Pa by SPAChain;
then consider f being Function of A,U such that
E1: f is bijective and
E1a: for x being set st x in A holds
x in f . x by A1, B1, ACpart1;
E1b: dom f = A by D1, FUNCT_2:def 1;
E1d: rng f = U by E1, FUNCT_2:def 3;
reconsider Pb = subrelstr (Lower A) as non empty transitive antisymmetric with_finite_stability# RelStr by D1;
A /\ (Lower A) = A by XBOOLE_1:21;
then A is StableSet of Pb by SPAChain;
then consider g being Function of A,L such that
G1: g is bijective and
G1a: for x being set st x in A holds
x in g . x by A1, C1, ACpart1;
G1b: dom g = A by D1, FUNCT_2:def 1;
G1d: rng g = L by G1, FUNCT_2:def 3;
set h = f .\/ g;
set C = rng (f .\/ g);
I1a: dom (f .\/ g) = (dom f) \/ (dom g) by LEXBFS:def 2;
Y1a: rng (f .\/ g) c= bool the carrier of R

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (f .\/ g) ; :: thesis:
then consider a being set such that
A2: a in dom (f .\/ g) and
B2: (f .\/ g) . a = x by FUNCT_1:def 5;
C2: (f .\/ g) . a = (f . a) \/ (g . a) by A2, I1a, LEXBFS:def 2;
f . a in U by A2, I1a, FUNCT_2:7;
then D2: f . a c= the carrier of R by S2d, XBOOLE_1:1;
g . a in L by A2, I1a, FUNCT_2:7;
then g . a c= the carrier of R by S2e, XBOOLE_1:1;
then x c= the carrier of R by B2, C2, D2, XBOOLE_1:8;
hence x in bool the carrier of R ; :: thesis:

end;

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

proof

now

let x be set ; :: thesis:

hereby :: thesis:

assume x in union (rng (f .\/ g)) ; :: thesis:
then consider Y being set such that
B2: x in Y and
C2: Y in rng (f .\/ g) by TARSKI:def 4;
consider a being set such that
D2: a in dom (f .\/ g) and
E2: Y = (f .\/ g) . a by C2, FUNCT_1:def 5;
F2: x in (f . a) \/ (g . a) by D2, E2, B2, I1a, LEXBFS:def 2;

per cases by F2, XBOOLE_0:def 3;

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

f . a in U by D2, I1a, FUNCT_2:7;
then x in Upper A by S2, S2d;
hence x in the carrier of R ; :: thesis:

end;

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

g . a in L by D2, I1a, FUNCT_2:7;
then x in Lower A by S2, S2e;
hence x in the carrier of R ; :: thesis:

end;

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

per cases by A2, XBOOLE_0:def 3;

suppose x in Upper A ; :: thesis:

then x in union U by S2d, EQREL_1:def 6;
then consider Y being set such that
A3: x in Y and
B3: Y in U by TARSKI:def 4;
consider a being set such that
C3: a in dom f and
D3: Y = f . a by B3, E1d, FUNCT_1:def 5;
E3: (f .\/ g) . a in rng (f .\/ g) by C3, I1a, E1b, G1b, FUNCT_1:12;
(f .\/ g) . a = (f . a) \/ (g . a) by C3, I1a, E1b, G1b, LEXBFS:def 2;
then x in (f .\/ g) . a by A3, D3, XBOOLE_0:def 3;
hence x in union (rng (f .\/ g)) by E3, TARSKI:def 4; :: thesis:

end;

suppose x in Lower A ; :: thesis:

then x in union L by S2e, EQREL_1:def 6;
then consider Y being set such that
A3: x in Y and
B3: Y in L by TARSKI:def 4;
consider a being set such that
C3: a in dom g and
D3: Y = g . a by B3, G1d, FUNCT_1:def 5;
E3: (f .\/ g) . a in rng (f .\/ g) by C3, I1a, E1b, G1b, FUNCT_1:12;
(f .\/ g) . a = (f . a) \/ (g . a) by C3, I1a, E1b, G1b, LEXBFS:def 2;
then x in (f .\/ g) . a by A3, D3, XBOOLE_0:def 3;
hence x in union (rng (f .\/ g)) by E3, TARSKI:def 4; :: thesis:

end;

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

end;

Y1c: now

let a be Subset of the carrier of R; :: thesis:
assume a in rng (f .\/ g) ; :: thesis:
then consider x being set such that
B2: x in dom (f .\/ g) and
C2: (f .\/ g) . x = a by FUNCT_1:def 5;
D2: (f .\/ g) . x = (f . x) \/ (g . x) by B2, I1a, LEXBFS:def 2;
set cfx = f . x;
set cgx = g . x;
E2: f . x in U by B2, I1a, FUNCT_2:7;
then reconsider cfx = f . x as Subset of Pa ;
E2g: g . x in L by B2, I1a, FUNCT_2:7;
then reconsider cgx = g . x as Subset of Pb ;
cfx <> {} by E2, EQREL_1:def 6;
hence a <> {} by C2, D2; :: thesis:
let b be Subset of the carrier of R; :: thesis:
assume b in rng (f .\/ g) ; :: thesis:
then consider y being set such that
B2y: y in dom (f .\/ g) and
C2y: (f .\/ g) . y = b by FUNCT_1:def 5;
D2y: (f .\/ g) . y = (f . y) \/ (g . y) by B2y, I1a, LEXBFS:def 2;
set cfy = f . y;
set cgy = g . y;
E2y: f . y in U by B2y, I1a, FUNCT_2:7;
then reconsider cfy = f . y as Subset of Pa ;
E2yg: g . y in L by B2y, I1a, FUNCT_2:7;
then reconsider cgy = g . y as Subset of Pb ;
assume FF2: a <> b ; :: thesis:
then F2a: cfx <> cfy by E1, C2, C2y, B2, B2y, I1a, E1b, FUNCT_1:def 8;
F2g: cgx <> cgy by G1, FF2, C2, C2y, B2, B2y, I1a, G1b, FUNCT_1:def 8;
assume a meets b ; :: thesis:
then a /\ b <> {} by XBOOLE_0:def 7;
then consider z being set such that
F2b: z in a /\ b by XBOOLE_0:def 1;
G2: z in a by F2b, XBOOLE_0:def 4;
H2: z in b by F2b, XBOOLE_0:def 4;
set cfz = f . z;
set cgz = g . z;

per cases by G2, H2, C2, C2y, D2, D2y, 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 by XBOOLE_0:def 7;
hence contradiction by E2, E2y, F2a, EQREL_1:def 6; :: thesis:

end;

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

then C3: z in A by S2d, S2e, ABAC0;
D3: z in f . z by S1, S2d, S2e, ABAC0, E1a;
E3: f . z in U by S1, S2d, S2e, ABAC0, FUNCT_2:7;
then reconsider cfz = f . z as Subset of Pa ;
z in cfx /\ cfz by S1, D3, XBOOLE_0:def 4;
then cfz meets cfx by XBOOLE_0:def 7;
then cfz = cfx by E2, E3, EQREL_1:def 6;
then F3: z = x by E1, B2, C3, I1a, E1b, FUNCT_1:def 8;
D3g: z in g . z by S1, S2d, S2e, ABAC0, G1a;
E3g: g . z in L by S1, S2d, S2e, ABAC0, FUNCT_2:7;
then reconsider cgz = g . z as Subset of Pb ;
z in cgz /\ cgy by S1, D3g, XBOOLE_0:def 4;
then cgz meets cgy by XBOOLE_0:def 7;
then cgz = cgy by E2yg, E3g, EQREL_1:def 6;
hence contradiction by F3, FF2, C2, C2y, G1, B2y, C3, I1a, G1b, FUNCT_1:def 8; :: thesis:

end;

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

then C3: z in A by S2d, S2e, ABAC0;
D3: z in f . z by S1, S2d, S2e, ABAC0, E1a;
E3: f . z in U by S1, S2d, S2e, ABAC0, FUNCT_2:7;
then reconsider cfz = f . z as Subset of Pa ;
z in cfy /\ cfz by S1, D3, XBOOLE_0:def 4;
then cfz meets cfy by XBOOLE_0:def 7;
then cfz = cfy by E2y, E3, EQREL_1:def 6;
then F3: z = y by E1, B2y, C3, I1a, E1b, FUNCT_1:def 8;
D3g: z in g . z by S1, S2d, S2e, ABAC0, G1a;
E3g: g . z in L by S1, S2d, S2e, ABAC0, FUNCT_2:7;
then reconsider cgz = g . z as Subset of Pb ;
z in cgz /\ cgx by S1, D3g, XBOOLE_0:def 4;
then cgz meets cgx by XBOOLE_0:def 7;
then cgz = cgx by E2g, E3g, EQREL_1:def 6;
hence contradiction by F3, FF2, C2, C2y, G1, B2, C3, I1a, G1b, FUNCT_1:def 8; :: thesis:

end;

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

then z in cgx /\ cgy by XBOOLE_0:def 4;
then cgx meets cgy by XBOOLE_0:def 7;
hence contradiction by E2g, E2yg, F2g, EQREL_1:def 6; :: thesis:

end;

Z1: 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 set such that
B2: x in dom (f .\/ g) and
C2: c = (f .\/ g) . x by FUNCT_1:def 5;
D2: c = (f . x) \/ (g . x) by B2, C2, I1a, LEXBFS:def 2;
set cf = f . x;
set cg = g . x;
f . x in U by B2, I1a, FUNCT_2:7;
then G2b: f . x is Clique of Pa by LCpart;
then G2a: f . x is Clique of R by SPClique;
g . x in L by B2, I1a, FUNCT_2:7;
then H2b: g . x is Clique of Pb by LCpart;
then H2a: g . x is Clique of R by SPClique;
then reconsider c9 = c as Subset of R by D2, G2a, XBOOLE_1:8;

now

let a, b be Element of R; :: thesis:
assume that
A3: a in c9 and
B3: b in c9 and
C3: a <> b ; :: thesis:
E3: x in f . x by B2, I1a, E1a;
F3: x in g . x by B2, I1a, G1a;
reconsider x = x as Element of R by B2, I1a, E1b, G1b;

per cases by A3, B3, D2, XBOOLE_0:def 3;

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

hence ( a <= b or b <= a ) by G2a, C3, DClique; :: thesis:

end;

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

then A4: ( x = a or x <= a ) by E3, B2, I1a, G2b, PabSmin;
( x = b or b <= x ) by F3, S1, B2, I1a, H2b, PbeSmax;
hence ( a <= b or b <= a ) by C3, A4, YELLOW_0:def 2; :: thesis:

end;

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

then A4: ( x = a or a <= x ) by F3, B2, I1a, H2b, PbeSmax;
( x = b or x <= b ) by E3, S1, B2, I1a, G2b, PabSmin;
hence ( a <= b or b <= a ) by C3, A4, YELLOW_0:def 2; :: thesis:

end;

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

hence ( a <= b or b <= a ) by H2a, C3, DClique; :: thesis:

end;

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

end;

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

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis:
assume that
A2: x1 in dom (f .\/ g) and
B2: x2 in dom (f .\/ g) and
C2: (f .\/ g) . x1 = (f .\/ g) . x2 ; :: thesis:
D2: (f .\/ g) . x1 is Clique of R by Z1, A2, FUNCT_1:12;
D2b: (f .\/ g) . x1 = (f . x1) \/ (g . x1) by I1a, A2, LEXBFS:def 2;
( x1 in f . x1 & x1 in g . x1 ) by A2, I1a, E1a, G1a;
then D2a: x1 in (f .\/ g) . x1 by D2b, XBOOLE_0:def 3;
E2b: (f .\/ g) . x2 = (f . x2) \/ (g . x2) by I1a, B2, LEXBFS:def 2;
( x2 in f . x2 & x2 in g . x2 ) by B2, I1a, E1a, G1a;
then x2 in (f .\/ g) . x2 by E2b, XBOOLE_0:def 3;
hence x1 = x2 by I1a, A2, B2, C2, D2, D2a, ACClique; :: thesis:

end;

reconsider C = rng (f .\/ g) as Clique-partition of R by Y1a, Y1b, Y1c, EQREL_1:def 6, Z1, LCpart;
take C ; :: thesis:
card C = card (f .\/ g) by H1, PRE_POLY:19
.= card A by I1a, E1b, G1b, CARD_1:104 ;
hence card C = stability# R by A1; :: thesis: