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 )
proof
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 ;
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 ;
A14: v1 in INTERSECTION (PB,PC) by ;
A15: not u in by ;
u = u3 /\ v1 by ;
then v1 <> {} by ;
then not v1 in by TARSKI:def 1;
then v1 in (INTERSECTION (PB,PC)) \ by ;
then A16: v in INTERSECTION (PA,PE) by ;
take v ; :: thesis: ( v in PA '/\' PE & u c= v )
thus ( v in PA '/\' PE & u c= v ) by ; :: thesis: 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 ; :: 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 ;
A25: u = (u1 /\ u3) /\ u4 by ;
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 ;
A29: not u in by ;
then v1 <> {} by ;
then not v1 in by TARSKI:def 1;
then v1 in (INTERSECTION (PA,PB)) \ by ;
then A30: v in INTERSECTION (PD,PC) by ;
take v ; :: thesis: ( v in PD '/\' PC & u c= v )
thus ( v in PD '/\' PC & u c= v ) by ; :: thesis: verum
end;
then PA '/\' PE '<' PD '/\' PC by SETFAM_1:def 2;
hence (PA '/\' PB) '/\' PC = PA '/\' (PB '/\' PC) by A1, A2, A17, Th4; :: thesis: verum