{} c= Y by XBOOLE_1:2;
then reconsider e = {{} } as Subset-Family of Y by ZFMISC_1:37;
set a = INTERSECTION PA,PB;
INTERSECTION PA,PB c= bool Y

proof

for z being set st z in INTERSECTION PA,PB holds
z in bool Y

proof

let z be set ; :: thesis: ( z in INTERSECTION PA,PB implies z in bool Y )
assume z in INTERSECTION PA,PB ; :: thesis: z in bool Y
then ex M, N being set st
( M in PA & N in PB & z = M /\ N ) by SETFAM_1:def 5;
then z c= Y by XBOOLE_1:108;
hence z in bool Y ; :: thesis: verum

end;

hence INTERSECTION PA,PB c= bool Y by TARSKI:def 3; :: thesis: verum

end;

then reconsider a = INTERSECTION PA,PB as Subset-Family of Y ;
reconsider ia = a \ e as Subset-Family of Y ;
A1: ( union PA = Y & union PB = Y ) by EQREL_1:def 6;
A2: union ia = union (INTERSECTION PA,PB) by Th3
.= (union PA) /\ (union PB) by SETFAM_1:39
.= Y by A1 ;
for A being Subset of Y st A in ia holds
( A <> {} & ( for B being Subset of Y holds
( not B in ia or A = B or A misses B ) ) )

proof

let A be Subset of Y; :: thesis: ( A in ia implies ( A <> {} & ( for B being Subset of Y holds
( not B in ia or A = B or A misses B ) ) ) )
assume A3: A in ia ; :: thesis: ( A <> {} & ( for B being Subset of Y holds
( not B in ia or A = B or A misses B ) ) )
then A4: not A in {{} } by XBOOLE_0:def 5;
A5: A in INTERSECTION PA,PB by A3, XBOOLE_0:def 5;
for B being Subset of Y holds
( not B in ia or A = B or A misses B )

proof

A6: for m, n, o, p being set holds (m /\ n) /\ (o /\ p) = m /\ ((n /\ o) /\ p)

proof

let m, n, o, p be set ; :: thesis: (m /\ n) /\ (o /\ p) = m /\ ((n /\ o) /\ p)
(m /\ n) /\ (o /\ p) = m /\ (n /\ (o /\ p)) by XBOOLE_1:16
.= m /\ ((n /\ o) /\ p) by XBOOLE_1:16 ;
hence (m /\ n) /\ (o /\ p) = m /\ ((n /\ o) /\ p) ; :: thesis: verum

end;

let B be Subset of Y; :: thesis: ( not B in ia or A = B or A misses B )
assume B in ia ; :: thesis: ( A = B or A misses B )
then B in INTERSECTION PA,PB by XBOOLE_0:def 5;
then consider M, N being set such that
A7: M in PA and
A8: N in PB and
A9: B = M /\ N by SETFAM_1:def 5;
consider S, T being set such that
A10: S in PA and
A11: T in PB and
A12: A = S /\ T by A5, SETFAM_1:def 5;
( M /\ N = S /\ T or not M = S or not N = T ) ;
then ( M /\ N = S /\ T or M misses S or N misses T ) by A7, A8, A10, A11, EQREL_1:def 6;
then A13: ( M /\ N = S /\ T or M /\ S = {} or N /\ T = {} ) by XBOOLE_0:def 7;
(M /\ S) /\ (N /\ T) = M /\ ((S /\ N) /\ T) by A6
.= (M /\ N) /\ (S /\ T) by A6 ;
hence ( A = B or A misses B ) by A9, A12, A13, XBOOLE_0:def 7; :: thesis: verum

end;

hence ( A <> {} & ( for B being Subset of Y holds
( not B in ia or A = B or A misses B ) ) ) by A4, TARSKI:def 1; :: thesis: verum

end;

hence (INTERSECTION PA,PB) \ {{} } is a_partition of Y by A2, EQREL_1:def 6; :: thesis: verum