let Y be non empty set ; :: thesis: 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; :: thesis: (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
;
A3:
PD '/\' PC '<' PA '/\' PE
proof
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 ;
:: thesis: ( u in PD '/\' PC implies ex v being set st
( v in PA '/\' PE & u c= v ) )
assume A4:
u in PD '/\' PC
;
:: thesis: 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 A17:
v in INTERSECTION PA,
PE
by A2, A8, A12, A14, SETFAM_1:def 5;
take
v
;
:: thesis: ( v in PA '/\' PE & u c= v )
thus
(
v in PA '/\' PE &
u c= v )
by A7, A10, A13, A16, A17, XBOOLE_0:def 5;
:: thesis: verum
end;
hence
PD '/\' PC '<' PA '/\' PE
by SETFAM_1:def 2;
:: thesis: verum
end;
PA '/\' PE '<' PD '/\' PC
proof
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 ;
:: thesis: ( u in PA '/\' PE implies ex v being set st
( v in PD '/\' PC & u c= v ) )
assume A18:
u in PA '/\' PE
;
:: thesis: 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
;
:: thesis: ( v in PD '/\' PC & u c= v )
thus
(
v in PD '/\' PC &
u c= v )
by A25, A27, A29, A30, XBOOLE_0:def 5;
:: thesis: verum
end;
hence
PA '/\' PE '<' PD '/\' PC
by SETFAM_1:def 2;
:: thesis: verum
end;
hence
(PA '/\' PB) '/\' PC = PA '/\' (PB '/\' PC)
by A1, A2, A3, Th5; :: thesis: verum