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

proof

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

end;

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

end;

hence ERl (PA '/\' PB) = (ERl PA) /\ (ERl PB) ; :: thesis: verum