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)
proof
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 ;
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 ;
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 ;
( 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 ;
y5 /\ z5 <> {} by ;
then A23: z5 in Cb by ;
Ca c= PA
proof
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;
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: ( 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 ;
y /\ z <> {} by ;
then z in Cb by ;
hence x1 in union Cb by ; :: thesis: verum
end;
union Cb c= pb
proof
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 ;
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 ;
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 ;
then A43: 1 <= len f by ;
A44: f . ((len fd) + 1) in y1 by ;
y1 meets q by ;
then consider z0 being object such that
A45: ( z0 in y1 & z0 in q ) by XBOOLE_0:3;
A46: z0 in y1 /\ q by ;
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: ( 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 ;
hence f . k = fd . k by FINSEQ_1:def 7; :: thesis: verum
end;
then A49: ( (fd ^ <*x1*>) . ((len fd) + 1) = x1 & f . 1 = x ) by ;
A50: f . (len fd) in q by ;
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: ( 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 ;
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 ; :: thesis: verum
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: ( 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 ;
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 ) ) )
per cases ( ( 1 <= i & i < len fd ) or ( 1 <= i & i = len fd ) ) by ;
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 )

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

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: verum
end;
end;
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: verum
end;
then pd in Ca by A35, A36, A42, A43, A49;
hence x1 in pb by ; :: thesis: verum
end;
then A57: pb = union Cb by ;
Cb c= PB
proof
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;
then A58: pb is_a_dependent_set_of PB by ;
now :: thesis: pb c= p0
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 ;
consider y1 being set such that
A61: x1 in y1 and
A62: y1 in Cb by ;
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 ;
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 ;
then A72: 1 <= len f by ;
A73: f . ((len fd) + 1) in y1 by ;
y1 meets q by ;
then consider z0 being object such that
A74: ( z0 in y1 & z0 in q ) by XBOOLE_0:3;
A75: z0 in y1 /\ q by ;
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: ( 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 ;
hence f . k = fd . k by FINSEQ_1:def 7; :: thesis: verum
end;
then A78: ( (fd ^ <*x1*>) . ((len fd) + 1) = x1 & f . 1 = x ) by ;
A79: f . (len fd) in q by ;
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: ( 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 ;
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 ; :: thesis: verum
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: ( 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 ;
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 ) ) )
per cases ( ( 1 <= i & i < len fd ) or ( 1 <= i & i = len fd ) ) by ;
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 )

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

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: verum
end;
end;
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: verum
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: ( 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 ;
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 ; :: thesis: verum
end;
hence contradiction by A7, A10, A11, A60, A71, A72, A78, Th21; :: thesis: verum
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 ;
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 ;
A102: f . ((len fd) + 1) in y1 by ;
y1 meets q by ;
then consider z0 being object such that
A103: ( z0 in y1 & z0 in q ) by XBOOLE_0:3;
A104: z0 in y1 /\ q by ;
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: ( 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 ;
hence f . k = fd . k by FINSEQ_1:def 7; :: thesis: verum
end;
then A107: f . (len fd) in q by ;
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: ( 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 ;
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 ; :: thesis: verum
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: ( 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 ;
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 ) ) )
per cases ( ( 1 <= i & i < len fd ) or ( 1 <= i & i = len fd ) ) by ;
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 )

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

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 ; :: thesis: verum
end;
end;
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: verum
end;
A115: ( (fd ^ <*y9*>) . ((len fd) + 1) = y & 1 <= len f ) by ;
A116: f . 1 = x by ;
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: ( 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 ;
A123: u in p2 by ;
reconsider x2 = f . i as set ;
reconsider y2 = f . (i + 1) as set ;
A124: [x2,u] in ERl PA by ;
A125: [u,y2] in ERl PB by ;
( 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 ; :: thesis: verum
end;
then [x9,y9] in (ERl PA) "\/" (ERl PB) by ;
hence [x,y] in (ERl PA) "\/" (ERl PB) ; :: thesis: verum
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: ( [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;
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) ) )
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;
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)
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 ;
hence [x1,x2] in ERl (PA '\/' PB) by ; :: thesis: verum
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: [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 ;
hence [x1,x2] in ERl (PA '\/' PB) by ; :: thesis: verum
end;
end;
end;
hence [x1,x2] in ERl (PA '\/' PB) ; :: thesis: verum
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: verum