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 A3:
u in PD '/\' PC
;
ex v being set st
( v in PA '/\' PE & u c= v )
then consider u1,
u2 being
set such that A4:
u1 in PD
and A5:
u2 in PC
and A6:
u = u1 /\ u2
by SETFAM_1:def 5;
consider u3,
u4 being
set such that A7:
u3 in PA
and A8:
u4 in PB
and A9:
u1 = u3 /\ u4
by A1, A4, SETFAM_1:def 5;
consider v,
v1,
v2 being
set such that A10:
v1 = u4 /\ u2
and A11:
v2 = u3
and A12:
v = (u3 /\ u4) /\ u2
;
A13:
v = v2 /\ v1
by A10, A11, A12, XBOOLE_1:16;
A14:
v1 in INTERSECTION (
PB,
PC)
by A5, A8, A10, SETFAM_1:def 5;
A15:
not
u in {{}}
by A3, XBOOLE_0:def 5;
u = u3 /\ v1
by A6, A9, A10, XBOOLE_1:16;
then
v1 <> {}
by A15, TARSKI:def 1;
then
not
v1 in {{}}
by TARSKI:def 1;
then
v1 in (INTERSECTION (PB,PC)) \ {{}}
by A14, XBOOLE_0:def 5;
then A16:
v in INTERSECTION (
PA,
PE)
by A2, A7, A11, A13, SETFAM_1:def 5;
take
v
;
( v in PA '/\' PE & u c= v )
thus
(
v in PA '/\' PE &
u c= v )
by A6, A9, A12, A15, A16, XBOOLE_0:def 5;
verum
end;
then A17:
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 A18:
u in PA '/\' PE
;
ex v being set st
( v in PD '/\' PC & u c= v )
then consider u1,
u2 being
set such that A19:
u1 in PA
and A20:
u2 in PE
and A21:
u = u1 /\ u2
by SETFAM_1:def 5;
consider u3,
u4 being
set such that A22:
u3 in PB
and A23:
u4 in PC
and A24:
u2 = u3 /\ u4
by A2, A20, SETFAM_1:def 5;
A25:
u = (u1 /\ u3) /\ u4
by A21, A24, XBOOLE_1:16;
consider v,
v1,
v2 being
set such that A26:
v1 = u1 /\ u3
and
v2 = u4
and A27:
v = (u1 /\ u3) /\ u4
;
A28:
v1 in INTERSECTION (
PA,
PB)
by A19, A22, A26, SETFAM_1:def 5;
A29:
not
u in {{}}
by A18, XBOOLE_0:def 5;
then
v1 <> {}
by A25, A26, TARSKI:def 1;
then
not
v1 in {{}}
by TARSKI:def 1;
then
v1 in (INTERSECTION (PA,PB)) \ {{}}
by A28, XBOOLE_0:def 5;
then A30:
v in INTERSECTION (
PD,
PC)
by A1, A23, A26, A27, SETFAM_1:def 5;
take
v
;
( v in PD '/\' PC & u c= v )
thus
(
v in PD '/\' PC &
u c= v )
by A25, A27, A29, A30, 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, A17, Th4; verum