let Y be non empty set ; :: thesis:
let PA, PB be a_partition of Y; :: thesis:
A1: PA is_finer_than PA '\/' PB by Th16;
A2: PB is_finer_than PA '\/' PB by Th16;
A3: union PA = Y by EQREL_1:def 4;
A4: union PB = Y by EQREL_1:def 4;
A5: ERl (PA '\/' PB) c= (ERl PA) "\/" (ERl PB)

let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume [x,y] in ERl (PA '\/' PB) ; :: thesis:
then consider p0 being Subset of Y such that
A6: p0 in PA '\/' PB and
A7: x in p0 and
A8: y in p0 by Def6;
A9: p0 is_min_depend PA,PB by A6, Def5;
then A10: p0 is_a_dependent_set_of PA ;
A11: p0 is_a_dependent_set_of PB by A9;
consider A1 being set such that
A12: A1 c= PA and
A1 <> {} and
A13: p0 = union A1 by A10;
consider a being set such that
A14: x in a and
A15: a in A1 by A7, A13, TARSKI:def 4;
reconsider Ca = { p where p is Element of PA : ex f being FinSequence of Y st
( 1 <= len f & f . 1 = x & f . (len f) in p & ( for i being Nat st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ) ) } as set ;
reconsider pb = union Ca as set ;
reconsider Cb = { p where p is Element of PB : ex q being set st
( q in Ca & p /\ q <> {} ) } as set ;
reconsider x9 = x as Element of Y by A7;
reconsider fx = <*x9*> as FinSequence of Y ;
A16: fx . 1 = x by FINSEQ_1:def 8;
then A17: fx . (len fx) in a by A14, FINSEQ_1:40;
( 1 <= len fx & ( for i being Nat st 1 <= i & i < len fx holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & fx . i in p1 & x0 in p1 /\ p2 & fx . (i + 1) in p2 ) ) ) by FINSEQ_1:40;
then A18: a in Ca by A12, A15, A16, A17;
then consider y5 being set such that
A19: x in y5 and
A20: y5 in Ca by A14;
consider z5 being set such that
A21: x9 in z5 and
A22: z5 in PB by A4, TARSKI:def 4;
y5 /\ z5 <> {} by A19, A21, XBOOLE_0:def 4;
then A23: z5 in Cb by A20, A22;
Ca c= PA

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in Ca ; :: thesis:
then ex p being Element of PA st
( z = p & ex f being FinSequence of Y st
( 1 <= len f & f . 1 = x & f . (len f) in p & ( for i being Nat st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ) ) ) ;
hence z in PA ; :: thesis:

end;

then A24: pb is_a_dependent_set_of PA by A18;
A25: pb c= union Cb

proof

let x1 be object ; :: according to TARSKI:def 3 :: thesis:
assume x1 in pb ; :: thesis:
then consider y being set such that
A26: x1 in y and
A27: y in Ca by TARSKI:def 4;
ex p being Element of PA st
( y = p & ex f being FinSequence of Y st
( 1 <= len f & f . 1 = x & f . (len f) in p & ( for i being Nat st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ) ) ) by A27;
then consider z being set such that
A28: x1 in z and
A29: z in PB by A4, A26, TARSKI:def 4;
y /\ z <> {} by A26, A28, XBOOLE_0:def 4;
then z in Cb by A27, A29;
hence x1 in union Cb by A28, TARSKI:def 4; :: thesis:

end;

union Cb c= pb

proof

let x1 be object ; :: according to TARSKI:def 3 :: thesis:
assume x1 in union Cb ; :: thesis:
then consider y1 being set such that
A30: x1 in y1 and
A31: y1 in Cb by TARSKI:def 4;
A32: ex p being Element of PB st
( y1 = p & ex q being set st
( q in Ca & p /\ q <> {} ) ) by A31;
then consider q being set such that
A33: q in Ca and
A34: y1 /\ q <> {} ;
consider pd being set such that
A35: x1 in pd and
A36: pd in PA by A3, A30, A32, TARSKI:def 4;
A37: ex pp being Element of PA st
( q = pp & ex f being FinSequence of Y st
( 1 <= len f & f . 1 = x & f . (len f) in pp & ( for i being Nat st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ) ) ) by A33;
then consider fd being FinSequence of Y such that
A38: 1 <= len fd and
A39: fd . 1 = x and
A40: fd . (len fd) in q and
A41: for i being Nat st 1 <= i & i < len fd holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & fd . i in p1 & x0 in p1 /\ p2 & fd . (i + 1) in p2 ) ;
reconsider x1 = x1 as Element of Y by A30, A32;
reconsider f = fd ^ <*x1*> as FinSequence of Y ;
len f = (len fd) + (len <*x1*>) by FINSEQ_1:22;
then A42: len f = (len fd) + 1 by FINSEQ_1:40;
1 + 1 <= (len fd) + 1 by A38, XREAL_1:6;
then A43: 1 <= len f by A42, XXREAL_0:2;
A44: f . ((len fd) + 1) in y1 by A30, FINSEQ_1:42;
y1 meets q by A34, XBOOLE_0:def 7;
then consider z0 being object such that
A45: ( z0 in y1 & z0 in q ) by XBOOLE_0:3;
A46: z0 in y1 /\ q by A45, XBOOLE_0:def 4;
A47: dom fd = Seg (len fd) by FINSEQ_1:def 3;
A48: for k being Nat st 1 <= k & k <= len fd holds
f . k = fd . k

proof

let k be Nat; :: thesis:
assume ( 1 <= k & k <= len fd ) ; :: thesis:
then k in dom fd by A47, FINSEQ_1:1;
hence f . k = fd . k by FINSEQ_1:def 7; :: thesis:

end;

then A49: ( (fd ^ <*x1*>) . ((len fd) + 1) = x1 & f . 1 = x ) by A38, A39, FINSEQ_1:42;
A50: f . (len fd) in q by A38, A40, A48;
A51: for i being Nat st 1 <= i & i < len fd holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )

proof

let i be Nat; :: thesis:
assume A52: ( 1 <= i & i < len fd ) ; :: thesis:
then A53: f . i = fd . i by A48;
( 1 <= i + 1 & i + 1 <= len fd ) by A52, NAT_1:13;
then f . (i + 1) = fd . (i + 1) by A48;
hence ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) by A41, A52, A53; :: thesis:

end;

for i being Nat st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )

proof

let i be Nat; :: thesis:
assume that
A54: 1 <= i and
A55: i < len f ; :: thesis:
A56: i <= len fd by A42, A55, NAT_1:13;

now :: thesis:

per cases by A54, A56, XXREAL_0:1;

case ( 1 <= i & i < len fd ) ; :: thesis:

hence ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) by A51; :: thesis:

end;

case ( 1 <= i & i = len fd ) ; :: thesis:

hence ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) by A32, A37, A44, A46, A50; :: thesis:

end;

hence ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ; :: thesis:

end;

then pd in Ca by A35, A36, A42, A43, A49;
hence x1 in pb by A35, TARSKI:def 4; :: thesis:

end;

then A57: pb = union Cb by A25, XBOOLE_0:def 10;
Cb c= PB

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in Cb ; :: thesis:
then ex p being Element of PB st
( z = p & ex q being set st
( q in Ca & p /\ q <> {} ) ) ;
hence z in PB ; :: thesis:

end;

then A58: pb is_a_dependent_set_of PB by A23, A57;

now :: thesis:

assume not pb c= p0 ; :: thesis:
then pb \ p0 <> {} by XBOOLE_1:37;
then consider x1 being object such that
A59: x1 in pb \ p0 by XBOOLE_0:def 1;
A60: not x1 in p0 by A59, XBOOLE_0:def 5;
consider y1 being set such that
A61: x1 in y1 and
A62: y1 in Cb by A57, A59, TARSKI:def 4;
A63: ex p being Element of PB st
( y1 = p & ex q being set st
( q in Ca & p /\ q <> {} ) ) by A62;
then consider q being set such that
A64: q in Ca and
A65: y1 /\ q <> {} ;
A66: ex pp being Element of PA st
( q = pp & ex f being FinSequence of Y st
( 1 <= len f & f . 1 = x & f . (len f) in pp & ( for i being Nat st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ) ) ) by A64;
then consider fd being FinSequence of Y such that
A67: 1 <= len fd and
A68: fd . 1 = x and
A69: fd . (len fd) in q and
A70: for i being Nat st 1 <= i & i < len fd holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & fd . i in p1 & x0 in p1 /\ p2 & fd . (i + 1) in p2 ) ;
reconsider x1 = x1 as Element of Y by A61, A63;
reconsider f = fd ^ <*x1*> as FinSequence of Y ;
len f = (len fd) + (len <*x1*>) by FINSEQ_1:22;
then A71: len f = (len fd) + 1 by FINSEQ_1:40;
1 + 1 <= (len fd) + 1 by A67, XREAL_1:6;
then A72: 1 <= len f by A71, XXREAL_0:2;
A73: f . ((len fd) + 1) in y1 by A61, FINSEQ_1:42;
y1 meets q by A65, XBOOLE_0:def 7;
then consider z0 being object such that
A74: ( z0 in y1 & z0 in q ) by XBOOLE_0:3;
A75: z0 in y1 /\ q by A74, XBOOLE_0:def 4;
A76: dom fd = Seg (len fd) by FINSEQ_1:def 3;
A77: for k being Nat st 1 <= k & k <= len fd holds
f . k = fd . k

proof

let k be Nat; :: thesis:
assume ( 1 <= k & k <= len fd ) ; :: thesis:
then k in dom fd by A76, FINSEQ_1:1;
hence f . k = fd . k by FINSEQ_1:def 7; :: thesis:

end;

then A78: ( (fd ^ <*x1*>) . ((len fd) + 1) = x1 & f . 1 = x ) by A67, A68, FINSEQ_1:42;
A79: f . (len fd) in q by A67, A69, A77;
A80: for i being Nat st 1 <= i & i < len fd holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )

proof

let i be Nat; :: thesis:
assume A81: ( 1 <= i & i < len fd ) ; :: thesis:
then A82: f . i = fd . i by A77;
( 1 <= i + 1 & i + 1 <= len fd ) by A81, NAT_1:13;
then f . (i + 1) = fd . (i + 1) by A77;
hence ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) by A70, A81, A82; :: thesis:

end;

A83: for i being Nat st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )

proof

let i be Nat; :: thesis:
assume that
A84: 1 <= i and
A85: i < len f ; :: thesis:
A86: i <= len fd by A71, A85, NAT_1:13;

now :: thesis:

per cases by A84, A86, XXREAL_0:1;

case ( 1 <= i & i < len fd ) ; :: thesis:

hence ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) by A80; :: thesis:

end;

case ( 1 <= i & i = len fd ) ; :: thesis:

hence ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) by A63, A66, A73, A75, A79; :: thesis:

end;

hence ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ; :: thesis:

end;

for i being Nat st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 & x0 in p2 & f . (i + 1) in p2 )

proof

let i be Nat; :: thesis:
assume ( 1 <= i & i < len f ) ; :: thesis:
then consider p1, p2, x0 being set such that
A87: ( p1 in PA & p2 in PB & f . i in p1 ) and
A88: x0 in p1 /\ p2 and
A89: f . (i + 1) in p2 by A83;
( x0 in p1 & x0 in p2 ) by A88, XBOOLE_0:def 4;
hence ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 & x0 in p2 & f . (i + 1) in p2 ) by A87, A89; :: thesis:

end;

hence contradiction by A7, A10, A11, A60, A71, A72, A78, Th21; :: thesis:

end;

then y in pb by A8, A9, A24, A58;
then consider y1 being set such that
A90: y in y1 and
A91: y1 in Cb by A25, TARSKI:def 4;
A92: ex p being Element of PB st
( y1 = p & ex q being set st
( q in Ca & p /\ q <> {} ) ) by A91;
then consider q being set such that
A93: q in Ca and
A94: y1 /\ q <> {} ;
A95: ex pp being Element of PA st
( q = pp & ex f being FinSequence of Y st
( 1 <= len f & f . 1 = x & f . (len f) in pp & ( for i being Nat st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ) ) ) by A93;
then consider fd being FinSequence of Y such that
A96: 1 <= len fd and
A97: fd . 1 = x and
A98: fd . (len fd) in q and
A99: for i being Nat st 1 <= i & i < len fd holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & fd . i in p1 & x0 in p1 /\ p2 & fd . (i + 1) in p2 ) ;
reconsider y9 = y as Element of Y by A8;
reconsider f = fd ^ <*y9*> as FinSequence of Y ;
len f = (len fd) + (len <*y9*>) by FINSEQ_1:22;
then A100: len f = (len fd) + 1 by FINSEQ_1:40;
then A101: 1 + 1 <= len f by A96, XREAL_1:6;
A102: f . ((len fd) + 1) in y1 by A90, FINSEQ_1:42;
y1 meets q by A94, XBOOLE_0:def 7;
then consider z0 being object such that
A103: ( z0 in y1 & z0 in q ) by XBOOLE_0:3;
A104: z0 in y1 /\ q by A103, XBOOLE_0:def 4;
A105: dom fd = Seg (len fd) by FINSEQ_1:def 3;
A106: for k being Nat st 1 <= k & k <= len fd holds
f . k = fd . k

proof

let k be Nat; :: thesis:
assume ( 1 <= k & k <= len fd ) ; :: thesis:
then k in dom fd by A105, FINSEQ_1:1;
hence f . k = fd . k by FINSEQ_1:def 7; :: thesis:

end;

then A107: f . (len fd) in q by A96, A98;
A108: for i being Nat st 1 <= i & i < len fd holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )

proof

let i be Nat; :: thesis:
assume A109: ( 1 <= i & i < len fd ) ; :: thesis:
then A110: f . i = fd . i by A106;
( 1 <= i + 1 & i + 1 <= len fd ) by A109, NAT_1:13;
then f . (i + 1) = fd . (i + 1) by A106;
hence ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) by A99, A109, A110; :: thesis:

end;

A111: for i being Nat st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )

proof

let i be Nat; :: thesis:
assume that
A112: 1 <= i and
A113: i < len f ; :: thesis:
A114: i <= len fd by A100, A113, NAT_1:13;

now :: thesis:

per cases by A112, A114, XXREAL_0:1;

case ( 1 <= i & i < len fd ) ; :: thesis:

hence ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) by A108; :: thesis:

end;

case ( 1 <= i & i = len fd ) ; :: thesis:

hence ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) by A92, A95, A102, A104, A107; :: thesis:

end;

hence ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ; :: thesis:

end;

A115: ( (fd ^ <*y9*>) . ((len fd) + 1) = y & 1 <= len f ) by A101, FINSEQ_1:42, XXREAL_0:2;
A116: f . 1 = x by A96, A97, A106;
for i being Nat st 1 <= i & i < len f holds
ex u being set st
( u in Y & [(f . i),u] in (ERl PA) \/ (ERl PB) & [u,(f . (i + 1))] in (ERl PA) \/ (ERl PB) )

proof

let i be Nat; :: thesis:
assume ( 1 <= i & i < len f ) ; :: thesis:
then consider p1, p2, u being set such that
A117: p1 in PA and
A118: p2 in PB and
A119: f . i in p1 and
A120: u in p1 /\ p2 and
A121: f . (i + 1) in p2 by A111;
A122: u in p1 by A120, XBOOLE_0:def 4;
A123: u in p2 by A120, XBOOLE_0:def 4;
reconsider x2 = f . i as set ;
reconsider y2 = f . (i + 1) as set ;
A124: [x2,u] in ERl PA by A117, A119, A122, Def6;
A125: [u,y2] in ERl PB by A118, A121, A123, Def6;
( ERl PA c= (ERl PA) \/ (ERl PB) & ERl PB c= (ERl PA) \/ (ERl PB) ) by XBOOLE_1:7;
hence ex u being set st
( u in Y & [(f . i),u] in (ERl PA) \/ (ERl PB) & [u,(f . (i + 1))] in (ERl PA) \/ (ERl PB) ) by A117, A122, A124, A125; :: thesis:

end;

then [x9,y9] in (ERl PA) "\/" (ERl PB) by A100, A115, A116, Th22;
hence [x,y] in (ERl PA) "\/" (ERl PB) ; :: thesis:

end;

for x1, x2 being object st [x1,x2] in (ERl PA) \/ (ERl PB) holds
[x1,x2] in ERl (PA '\/' PB)

proof

let x1, x2 be object ; :: thesis:
assume [x1,x2] in (ERl PA) \/ (ERl PB) ; :: thesis:
then ( [x1,x2] in ERl PA or [x1,x2] in ERl PB ) by XBOOLE_0:def 3;
then A126: ( ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) or ex B being Subset of Y st
( B in PB & x1 in B & x2 in B ) ) by Def6;

now :: thesis:

per cases by A126;

case ( x1 in Y & x2 in Y & ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) ; :: thesis:

then consider A being Subset of Y such that
A127: A in PA and
A128: ( x1 in A & x2 in A ) ;
ex y being set st
( y in PA '\/' PB & A c= y ) by A1, A127, SETFAM_1:def 2;
hence [x1,x2] in ERl (PA '\/' PB) by A128, Def6; :: thesis:

end;

case ( x1 in Y & x2 in Y & ex B being Subset of Y st
( B in PB & x1 in B & x2 in B ) ) ; :: thesis:

then consider B being Subset of Y such that
A129: B in PB and
A130: ( x1 in B & x2 in B ) ;
ex y being set st
( y in PA '\/' PB & B c= y ) by A2, A129, SETFAM_1:def 2;
hence [x1,x2] in ERl (PA '\/' PB) by A130, Def6; :: thesis:

end;

hence [x1,x2] in ERl (PA '\/' PB) ; :: thesis:

end;

then (ERl PA) \/ (ERl PB) c= ERl (PA '\/' PB) ;
then (ERl PA) "\/" (ERl PB) c= ERl (PA '\/' PB) by EQREL_1:def 2;
hence ERl (PA '\/' PB) = (ERl PA) "\/" (ERl PB) by A5; :: thesis: