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 by Th17;
A2: 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
A5: C in PA '/\' PB and
A6: ( x1 in C & x2 in C ) by Def6;
A7: ex A being set st
( A in PA & C c= A ) by A1, A5, SETFAM_1:def 2;
A8: ex B being set st
( B in PB & C c= B ) by A2, A5, SETFAM_1:def 2;
A9: [x1,x2] in ERl PA by A6, A7, Def6;
[x1,x2] in ERl PB by A6, A8, Def6;
hence [x1,x2] in (ERl PA) /\ (ERl PB) by A9, XBOOLE_0:def 4; :: thesis: verum

end;

assume A11: [x1,x2] in (ERl PA) /\ (ERl PB) ; :: thesis: [x1,x2] in ERl (PA '/\' PB)
then A12: [x1,x2] in ERl PA by XBOOLE_0:def 4;
A13: [x1,x2] in ERl PB by A11, XBOOLE_0:def 4;
consider A being Subset of Y such that
A14: A in PA and
A15: x1 in A and
A16: x2 in A by A12, Def6;
consider B being Subset of Y such that
A17: B in PB and
A18: x1 in B and
A19: x2 in B by A13, Def6;
A20: A /\ B <> {} by A15, A18, XBOOLE_0:def 4;
consider C being Subset of Y such that
A21: C = A /\ B ;
A22: C in INTERSECTION (PA,PB) by A14, A17, A21, SETFAM_1:def 5;
not C in {{}} by A20, A21, TARSKI:def 1;
then A24: C in (INTERSECTION (PA,PB)) \ {{}} by A22, XBOOLE_0:def 5;
( x1 in C & x2 in C ) by A15, A16, A18, A19, A21, XBOOLE_0:def 4;
hence [x1,x2] in ERl (PA '/\' PB) by A24, Def6; :: thesis: verum

end;

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