let Y be non empty set ; for PA, PB, PC being a_partition of Y holds (PA '/\' PB) '/\' PC = PA '/\' (PB '/\' PC)
let PA, PB, PC be a_partition of Y; (PA '/\' PB) '/\' PC = PA '/\' (PB '/\' PC)
consider PD, PE being a_partition of Y such that
A1:
PD = PA '/\' PB
and
A2:
PE = PB '/\' PC
;
for u being set st u in PD '/\' PC holds
ex v being set st
( v in PA '/\' PE & u c= v )
proof
let u be
set ;
( u in PD '/\' PC implies ex v being set st
( v in PA '/\' PE & u c= v ) )
assume A4:
u in PD '/\' PC
;
ex v being set st
( v in PA '/\' PE & u c= v )
then consider u1,
u2 being
set such that A5:
u1 in PD
and A6:
u2 in PC
and A7:
u = u1 /\ u2
by SETFAM_1:def 5;
consider u3,
u4 being
set such that A8:
u3 in PA
and A9:
u4 in PB
and A10:
u1 = u3 /\ u4
by A1, A5, SETFAM_1:def 5;
consider v,
v1,
v2 being
set such that A11:
v1 = u4 /\ u2
and A12:
v2 = u3
and A13:
v = (u3 /\ u4) /\ u2
;
A14:
v = v2 /\ v1
by A11, A12, A13, XBOOLE_1:16;
A15:
v1 in INTERSECTION (
PB,
PC)
by A6, A9, A11, SETFAM_1:def 5;
A16:
not
u in {{}}
by A4, XBOOLE_0:def 5;
u = u3 /\ v1
by A7, A10, A11, XBOOLE_1:16;
then
v1 <> {}
by A16, TARSKI:def 1;
then
not
v1 in {{}}
by TARSKI:def 1;
then
v1 in (INTERSECTION (PB,PC)) \ {{}}
by A15, XBOOLE_0:def 5;
then A21:
v in INTERSECTION (
PA,
PE)
by A2, A8, A12, A14, SETFAM_1:def 5;
take
v
;
( v in PA '/\' PE & u c= v )
thus
(
v in PA '/\' PE &
u c= v )
by A7, A10, A13, A16, A21, XBOOLE_0:def 5;
verum
end;
then A22:
PD '/\' PC '<' PA '/\' PE
by SETFAM_1:def 2;
for u being set st u in PA '/\' PE holds
ex v being set st
( v in PD '/\' PC & u c= v )
proof
let u be
set ;
( u in PA '/\' PE implies ex v being set st
( v in PD '/\' PC & u c= v ) )
assume A24:
u in PA '/\' PE
;
ex v being set st
( v in PD '/\' PC & u c= v )
then consider u1,
u2 being
set such that A25:
u1 in PA
and A26:
u2 in PE
and A27:
u = u1 /\ u2
by SETFAM_1:def 5;
consider u3,
u4 being
set such that A28:
u3 in PB
and A29:
u4 in PC
and A30:
u2 = u3 /\ u4
by A2, A26, SETFAM_1:def 5;
A31:
u = (u1 /\ u3) /\ u4
by A27, A30, XBOOLE_1:16;
consider v,
v1,
v2 being
set such that A32:
v1 = u1 /\ u3
and
v2 = u4
and A33:
v = (u1 /\ u3) /\ u4
;
A34:
v1 in INTERSECTION (
PA,
PB)
by A25, A28, A32, SETFAM_1:def 5;
A35:
not
u in {{}}
by A24, XBOOLE_0:def 5;
then
v1 <> {}
by A31, A32, TARSKI:def 1;
then
not
v1 in {{}}
by TARSKI:def 1;
then
v1 in (INTERSECTION (PA,PB)) \ {{}}
by A34, XBOOLE_0:def 5;
then A39:
v in INTERSECTION (
PD,
PC)
by A1, A29, A32, A33, SETFAM_1:def 5;
take
v
;
( v in PD '/\' PC & u c= v )
thus
(
v in PD '/\' PC &
u c= v )
by A31, A33, A35, A39, XBOOLE_0:def 5;
verum
end;
then
PA '/\' PE '<' PD '/\' PC
by SETFAM_1:def 2;
hence
(PA '/\' PB) '/\' PC = PA '/\' (PB '/\' PC)
by A1, A2, A22, Th5; verum