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 ;
A6: ex B being set st
( B in PB & C c= B ) by ;
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 ; :: 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 ;
consider A being Subset of Y such that
A11: A in PA and
A12: x1 in A and
A13: x2 in A by ;
consider B being Subset of Y such that
A14: B in PB and
A15: x1 in B and
A16: x2 in B by ;
A17: A /\ B <> {} by ;
consider C being Subset of Y such that
A18: C = A /\ B ;
A19: C in INTERSECTION (PA,PB) by ;
not C in by ;
then A20: C in (INTERSECTION (PA,PB)) \ by ;
( x1 in C & x2 in C ) by ;
hence [x1,x2] in ERl (PA '/\' PB) by ; :: thesis: verum
end;
hence ERl (PA '/\' PB) = (ERl PA) /\ (ERl PB) ; :: thesis: verum