let Y be non empty set ; for PA, PB being a_partition of Y holds ERl (PA '/\' PB) = (ERl PA) /\ (ERl PB)
let PA, PB be a_partition of Y; 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 ;
( [x1,x2] in ERl (PA '/\' PB) iff [x1,x2] in (ERl PA) /\ (ERl PB) )
hereby ( [x1,x2] in (ERl PA) /\ (ERl PB) implies [x1,x2] in ERl (PA '/\' PB) )
assume
[x1,x2] in ERl (PA '/\' PB)
;
[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;
verum
end;
assume A8:
[x1,x2] in (ERl PA) /\ (ERl PB)
;
[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;
verum
end;
hence
ERl (PA '/\' PB) = (ERl PA) /\ (ERl PB)
; verum