A1: {} c= Y by XBOOLE_1:2;
reconsider e = {{} } as Subset-Family of Y by A1, ZFMISC_1:37;
set a = INTERSECTION PA,PB;
A2: 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 A3: z in INTERSECTION PA,PB ; :: thesis: z in bool Y
A4: ex M, N being set st
( M in PA & N in PB & z = M /\ N ) by A3, SETFAM_1:def 5;
A5: z c= Y by A4, XBOOLE_1:108;
thus z in bool Y by A5; :: thesis: verum

end;

reconsider a = INTERSECTION PA,PB as Subset-Family of Y by A2, TARSKI:def 3;
reconsider ia = a \ e as Subset-Family of Y ;
A6: ( union PA = Y & union PB = Y ) by EQREL_1:def 6;
A7: union ia = union (INTERSECTION PA,PB) by Th3
.= (union PA) /\ (union PB) by SETFAM_1:39
.= Y by A6 ;
A8: 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 A9: A in ia ; :: thesis: ( A <> {} & ( for B being Subset of Y holds
( not B in ia or A = B or A misses B ) ) )
A10: not A in {{} } by A9, XBOOLE_0:def 5;
A11: A in INTERSECTION PA,PB by A9, XBOOLE_0:def 5;
A12: for B being Subset of Y holds
( not B in ia or A = B or A misses B )

proof

A13: 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)
A14: (m /\ n) /\ (o /\ p) = m /\ (n /\ (o /\ p)) by XBOOLE_1:16
.= m /\ ((n /\ o) /\ p) by XBOOLE_1:16 ;
thus (m /\ n) /\ (o /\ p) = m /\ ((n /\ o) /\ p) by A14; :: thesis: verum

end;

let B be Subset of Y; :: thesis: ( not B in ia or A = B or A misses B )
assume A15: B in ia ; :: thesis: ( A = B or A misses B )
A16: B in INTERSECTION PA,PB by A15, XBOOLE_0:def 5;
consider M, N being set such that
A17: ( M in PA & N in PB ) and
A18: B = M /\ N by A16, SETFAM_1:def 5;
consider S, T being set such that
A19: ( S in PA & T in PB ) and
A20: A = S /\ T by A11, SETFAM_1:def 5;
A21: ( M /\ N = S /\ T or not M = S or not N = T ) ;
A22: ( M /\ N = S /\ T or M misses S or N misses T ) by A17, A19, A21, EQREL_1:def 6;
A23: ( M /\ N = S /\ T or M /\ S = {} or N /\ T = {} ) by A22, XBOOLE_0:def 7;
A24: (M /\ S) /\ (N /\ T) = M /\ ((S /\ N) /\ T) by A13
.= (M /\ N) /\ (S /\ T) by A13 ;
thus ( A = B or A misses B ) by A18, A20, A23, A24, XBOOLE_0:def 7; :: thesis: verum

end;

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

end;

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