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

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

hence
ERl (PA '/\' PB) = (ERl PA) /\ (ERl PB)
; :: thesis: verum
let x1, x2 be object ; :: thesis: ( [x1,x2] in ERl (PA '/\' PB) iff [x1,x2] in (ERl PA) /\ (ERl 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;hereby :: thesis: ( [x1,x2] in (ERl PA) /\ (ERl PB) implies [x1,x2] in ERl (PA '/\' PB) )

assume A8:
[x1,x2] in (ERl PA) /\ (ERl PB)
; :: thesis: [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;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

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