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 '>' PA '/\' PB & PB '>' PA '/\' PB ) by Th17;
for x1, x2 being set holds
( [x1,x2] in ERl (PA '/\' PB) iff [x1,x2] in (ERl PA) /\ (ERl PB) )

proof

let x1, x2 be set ; :: thesis: ( [x1,x2] in ERl (PA '/\' PB) iff [x1,x2] in (ERl PA) /\ (ERl PB) )

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

assume [x1,x2] in ERl (PA '/\' PB) ; :: thesis: [x1,x2] in (ERl PA) /\ (ERl PB)
then consider C being Subset of Y such that
A2: ( C in PA '/\' PB & x1 in C & x2 in C ) by Def6;
consider A being set such that
A3: ( A in PA & C c= A ) by A1, A2, SETFAM_1:def 2;
consider B being set such that
A4: ( B in PB & C c= B ) by A1, A2, SETFAM_1:def 2;
( [x1,x2] in ERl PA & [x1,x2] in ERl PB ) by A2, A3, A4, Def6;
hence [x1,x2] in (ERl PA) /\ (ERl PB) by XBOOLE_0:def 4; :: thesis: verum

end;

assume [x1,x2] in (ERl PA) /\ (ERl PB) ; :: thesis: [x1,x2] in ERl (PA '/\' PB)
then A5: ( [x1,x2] in ERl PA & [x1,x2] in ERl PB ) by XBOOLE_0:def 4;
then consider A being Subset of Y such that
A6: ( A in PA & x1 in A & x2 in A ) by Def6;
consider B being Subset of Y such that
A7: ( B in PB & x1 in B & x2 in B ) by A5, Def6;
A8: A /\ B <> {} by A6, A7, XBOOLE_0:def 4;
consider C being Subset of Y such that
A9: C = A /\ B ;
A10: C in INTERSECTION PA,PB by A6, A7, A9, SETFAM_1:def 5;
not C in {{} } by A8, A9, TARSKI:def 1;
then A11: C in (INTERSECTION PA,PB) \ {{} } by A10, XBOOLE_0:def 5;
A12: x1 in C by A6, A7, A9, XBOOLE_0:def 4;
x2 in C by A6, A7, A9, XBOOLE_0:def 4;
hence [x1,x2] in ERl (PA '/\' PB) by A11, A12, Def6; :: thesis: verum

end;

hence ERl (PA '/\' PB) = (ERl PA) /\ (ERl PB) by RELAT_1:def 2; :: thesis: verum