let Y be non empty set ; :: thesis: for PA, PB being a_partition of Y holds ERl (PA '\/' PB) = (ERl PA) "\/" (ERl PB)

let PA, PB be a_partition of Y; :: thesis: ERl (PA '\/' PB) = (ERl PA) "\/" (ERl PB)

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)

[x1,x2] in 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: verum

let PA, PB be a_partition of Y; :: thesis: ERl (PA '\/' PB) = (ERl PA) "\/" (ERl PB)

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)

proof

for x1, x2 being object st [x1,x2] in (ERl PA) \/ (ERl PB) holds
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in ERl (PA '\/' PB) or [x,y] in (ERl PA) "\/" (ERl PB) )

assume [x,y] in ERl (PA '\/' PB) ; :: thesis: [x,y] in (ERl PA) "\/" (ERl PB)

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

A25: pb c= union Cb

Cb c= PB

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

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 )

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 )

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) )

hence [x,y] in (ERl PA) "\/" (ERl PB) ; :: thesis: verum

end;assume [x,y] in ERl (PA '\/' PB) ; :: thesis: [x,y] in (ERl PA) "\/" (ERl PB)

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

proof

then A24:
pb is_a_dependent_set_of PA
by A18;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Ca or z in PA )

assume z in Ca ; :: thesis: z in PA

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: verum

end;assume z in Ca ; :: thesis: z in PA

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: verum

A25: pb c= union Cb

proof

union Cb c= pb
let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in pb or x1 in union Cb )

assume x1 in pb ; :: thesis: x1 in union Cb

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: verum

end;assume x1 in pb ; :: thesis: x1 in union Cb

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: verum

proof

then A57:
pb = union Cb
by A25, XBOOLE_0:def 10;
let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in union Cb or x1 in pb )

assume x1 in union Cb ; :: thesis: x1 in pb

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

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 )

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 x1 in pb by A35, TARSKI:def 4; :: thesis: verum

end;assume x1 in union Cb ; :: thesis: x1 in pb

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

then A49:
( (fd ^ <*x1*>) . ((len fd) + 1) = x1 & f . 1 = x )
by A38, A39, FINSEQ_1:42;
let k be Nat; :: thesis: ( 1 <= k & k <= len fd implies f . k = fd . k )

assume ( 1 <= k & k <= len fd ) ; :: thesis: f . k = fd . k

then k in dom fd by A47, FINSEQ_1:1;

hence f . k = fd . k by FINSEQ_1:def 7; :: thesis: verum

end;assume ( 1 <= k & k <= len fd ) ; :: thesis: f . k = fd . k

then k in dom fd by A47, FINSEQ_1:1;

hence f . k = fd . k by FINSEQ_1:def 7; :: thesis: verum

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

for i being Nat st 1 <= i & i < len f holds
let i be Nat; :: thesis: ( 1 <= i & i < len fd implies 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 ) )

assume A52: ( 1 <= i & i < len fd ) ; :: thesis: 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 )

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: verum

end;( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) )

assume A52: ( 1 <= i & i < len fd ) ; :: thesis: 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 )

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: verum

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

then
pd in Ca
by A35, A36, A42, A43, A49;
let i be Nat; :: thesis: ( 1 <= i & i < len f implies 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 ) )

assume that

A54: 1 <= i and

A55: i < len f ; :: thesis: 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 )

A56: i <= len fd by A42, A55, NAT_1:13;

( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ; :: thesis: verum

end;( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) )

assume that

A54: 1 <= i and

A55: i < len f ; :: thesis: 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 )

A56: i <= len fd by A42, A55, NAT_1:13;

now :: thesis: ( ( 1 <= i & i < len fd & 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 ) ) or ( 1 <= i & i = len fd & 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 ) ) )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 ) ) or ( 1 <= i & i = len fd & 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 ) ) )

per cases
( ( 1 <= i & i < len fd ) or ( 1 <= i & i = len fd ) )
by A54, A56, XXREAL_0:1;

end;

( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ; :: thesis: verum

hence x1 in pb by A35, TARSKI:def 4; :: thesis: verum

Cb c= PB

proof

then A58:
pb is_a_dependent_set_of PB
by A23, A57;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Cb or z in PB )

assume z in Cb ; :: thesis: z in PB

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: verum

end;assume z in Cb ; :: thesis: z in PB

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: verum

now :: thesis: pb c= p0

then
y in pb
by A8, A9, A24, A58;assume
not pb c= p0
; :: thesis: contradiction

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

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 )

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 )

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 )

end;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

then A78:
( (fd ^ <*x1*>) . ((len fd) + 1) = x1 & f . 1 = x )
by A67, A68, FINSEQ_1:42;
let k be Nat; :: thesis: ( 1 <= k & k <= len fd implies f . k = fd . k )

assume ( 1 <= k & k <= len fd ) ; :: thesis: f . k = fd . k

then k in dom fd by A76, FINSEQ_1:1;

hence f . k = fd . k by FINSEQ_1:def 7; :: thesis: verum

end;assume ( 1 <= k & k <= len fd ) ; :: thesis: f . k = fd . k

then k in dom fd by A76, FINSEQ_1:1;

hence f . k = fd . k by FINSEQ_1:def 7; :: thesis: verum

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

A83:
for i being Nat st 1 <= i & i < len f holds
let i be Nat; :: thesis: ( 1 <= i & i < len fd implies 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 ) )

assume A81: ( 1 <= i & i < len fd ) ; :: thesis: 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 )

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: verum

end;( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) )

assume A81: ( 1 <= i & i < len fd ) ; :: thesis: 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 )

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: verum

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

for i being Nat st 1 <= i & i < len f holds
let i be Nat; :: thesis: ( 1 <= i & i < len f implies 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 ) )

assume that

A84: 1 <= i and

A85: i < len f ; :: thesis: 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 )

A86: i <= len fd by A71, A85, NAT_1:13;

( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ; :: thesis: verum

end;( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) )

assume that

A84: 1 <= i and

A85: i < len f ; :: thesis: 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 )

A86: i <= len fd by A71, A85, NAT_1:13;

now :: thesis: ( ( 1 <= i & i < len fd & 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 ) ) or ( 1 <= i & i = len fd & 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 ) ) )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 ) ) or ( 1 <= i & i = len fd & 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 ) ) )

per cases
( ( 1 <= i & i < len fd ) or ( 1 <= i & i = len fd ) )
by A84, A86, XXREAL_0:1;

end;

( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ; :: thesis: verum

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

hence
contradiction
by A7, A10, A11, A60, A71, A72, A78, Th21; :: thesis: verum
let i be Nat; :: thesis: ( 1 <= i & i < len f implies 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 ) )

assume ( 1 <= i & i < len f ) ; :: thesis: 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 )

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: verum

end;( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 & x0 in p2 & f . (i + 1) in p2 ) )

assume ( 1 <= i & i < len f ) ; :: thesis: 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 )

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: verum

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

then A107:
f . (len fd) in q
by A96, A98;
let k be Nat; :: thesis: ( 1 <= k & k <= len fd implies f . k = fd . k )

assume ( 1 <= k & k <= len fd ) ; :: thesis: f . k = fd . k

then k in dom fd by A105, FINSEQ_1:1;

hence f . k = fd . k by FINSEQ_1:def 7; :: thesis: verum

end;assume ( 1 <= k & k <= len fd ) ; :: thesis: f . k = fd . k

then k in dom fd by A105, FINSEQ_1:1;

hence f . k = fd . k by FINSEQ_1:def 7; :: thesis: verum

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

A111:
for i being Nat st 1 <= i & i < len f holds
let i be Nat; :: thesis: ( 1 <= i & i < len fd implies 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 ) )

assume A109: ( 1 <= i & i < len fd ) ; :: thesis: 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 )

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: verum

end;( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) )

assume A109: ( 1 <= i & i < len fd ) ; :: thesis: 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 )

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: verum

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

A115:
( (fd ^ <*y9*>) . ((len fd) + 1) = y & 1 <= len f )
by A101, FINSEQ_1:42, XXREAL_0:2;
let i be Nat; :: thesis: ( 1 <= i & i < len f implies 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 ) )

assume that

A112: 1 <= i and

A113: i < len f ; :: thesis: 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 )

A114: i <= len fd by A100, A113, NAT_1:13;

( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ; :: thesis: verum

end;( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) )

assume that

A112: 1 <= i and

A113: i < len f ; :: thesis: 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 )

A114: i <= len fd by A100, A113, NAT_1:13;

now :: thesis: ( ( 1 <= i & i < len fd & 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 ) ) or ( 1 <= i & i = len fd & 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 ) ) )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 ) ) or ( 1 <= i & i = len fd & 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 ) ) )

per cases
( ( 1 <= i & i < len fd ) or ( 1 <= i & i = len fd ) )
by A112, A114, XXREAL_0:1;

end;

case
( 1 <= i & i < len fd )
; :: thesis: 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 )

( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )

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: verum

end;( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) by A108; :: thesis: verum

case
( 1 <= i & i = len fd )
; :: thesis: 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 )

( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )

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: verum

end;( 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: verum

( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ; :: thesis: verum

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

then
[x9,y9] in (ERl PA) "\/" (ERl PB)
by A100, A115, A116, Th22;
let i be Nat; :: thesis: ( 1 <= i & i < len f implies 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) ) )

assume ( 1 <= i & i < len f ) ; :: thesis: 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) )

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: verum

end;( u in Y & [(f . i),u] in (ERl PA) \/ (ERl PB) & [u,(f . (i + 1))] in (ERl PA) \/ (ERl PB) ) )

assume ( 1 <= i & i < len f ) ; :: thesis: 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) )

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: verum

hence [x,y] in (ERl PA) "\/" (ERl PB) ; :: thesis: verum

[x1,x2] in ERl (PA '\/' PB)

proof

then
(ERl PA) \/ (ERl PB) c= ERl (PA '\/' PB)
;
let x1, x2 be object ; :: thesis: ( [x1,x2] in (ERl PA) \/ (ERl PB) implies [x1,x2] in ERl (PA '\/' PB) )

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

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;

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

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: ( ( x1 in Y & x2 in Y & ex A being Subset of Y st

( A in PA & x1 in A & x2 in A ) & [x1,x2] in ERl (PA '\/' PB) ) or ( x1 in Y & x2 in Y & ex B being Subset of Y st

( B in PB & x1 in B & x2 in B ) & [x1,x2] in ERl (PA '\/' PB) ) )end;

hence
[x1,x2] in ERl (PA '\/' PB)
; :: thesis: verum( A in PA & x1 in A & x2 in A ) & [x1,x2] in ERl (PA '\/' PB) ) or ( x1 in Y & x2 in Y & ex B being Subset of Y st

( B in PB & x1 in B & x2 in B ) & [x1,x2] in ERl (PA '\/' PB) ) )

per cases
( ( x1 in Y & x2 in Y & ex A being Subset of Y st

( A in PA & x1 in A & x2 in A ) ) or ( x1 in Y & x2 in Y & ex B being Subset of Y st

( B in PB & x1 in B & x2 in B ) ) ) by A126;

end;

( A in PA & x1 in A & x2 in A ) ) or ( x1 in Y & x2 in Y & ex B being Subset of Y st

( B in PB & x1 in B & x2 in B ) ) ) 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: [x1,x2] in ERl (PA '\/' PB)

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

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: verum

end;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: verum

case
( x1 in Y & x2 in Y & ex B being Subset of Y st

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

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

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: verum

end;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: verum

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: verum