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 ;

for u being set st u in PD '/\' PC holds

ex v being set st

( v in PA '/\' PE & u c= v )

for u being set st u in PA '/\' PE holds

ex v being set st

( v in PD '/\' PC & u c= v )

hence (PA '/\' PB) '/\' PC = PA '/\' (PB '/\' PC) by A1, A2, A17, Th4; :: thesis: verum

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 ;

for u being set st u in PD '/\' PC holds

ex v being set st

( v in PA '/\' PE & u c= v )

proof

then A17:
PD '/\' PC '<' PA '/\' PE
by SETFAM_1:def 2;
let u be set ; :: thesis: ( u in PD '/\' PC implies ex v being set st

( v in PA '/\' PE & u c= v ) )

assume A3: 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

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 ; :: thesis: ( 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; :: thesis: verum

end;( v in PA '/\' PE & u c= v ) )

assume A3: 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

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 ; :: thesis: ( 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; :: thesis: verum

for u being set st u in PA '/\' PE holds

ex v being set st

( v in PD '/\' PC & u c= v )

proof

then
PA '/\' PE '<' PD '/\' PC
by SETFAM_1:def 2;
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;( 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

hence (PA '/\' PB) '/\' PC = PA '/\' (PB '/\' PC) by A1, A2, A17, Th4; :: thesis: verum