{} c= Y
;

then reconsider e = {{}} as Subset-Family of Y by ZFMISC_1:31;

set a = INTERSECTION (PA,PB);

for z being object st z in INTERSECTION (PA,PB) holds

z in bool Y

reconsider ia = a \ e as Subset-Family of Y ;

A1: ( union PA = Y & union PB = Y ) by EQREL_1:def 4;

A2: union ia = union (INTERSECTION (PA,PB)) by Th2

.= (union PA) /\ (union PB) by SETFAM_1:28

.= 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 ) ) )

then reconsider e = {{}} as Subset-Family of Y by ZFMISC_1:31;

set a = INTERSECTION (PA,PB);

for z being object st z in INTERSECTION (PA,PB) holds

z in bool Y

proof

then reconsider a = INTERSECTION (PA,PB) as Subset-Family of Y by TARSKI:def 3;
let z be object ; :: thesis: ( z in INTERSECTION (PA,PB) implies z in bool Y )

reconsider zz = z as set by TARSKI:1;

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 zz c= Y by XBOOLE_1:108;

hence z in bool Y ; :: thesis: verum

end;reconsider zz = z as set by TARSKI:1;

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 zz c= Y by XBOOLE_1:108;

hence z in bool Y ; :: thesis: verum

reconsider ia = a \ e as Subset-Family of Y ;

A1: ( union PA = Y & union PB = Y ) by EQREL_1:def 4;

A2: union ia = union (INTERSECTION (PA,PB)) by Th2

.= (union PA) /\ (union PB) by SETFAM_1:28

.= 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

hence
(INTERSECTION (PA,PB)) \ {{}} is a_partition of Y
by A2, EQREL_1:def 4; :: thesis: verum
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 )

( not B in ia or A = B or A misses B ) ) ) by A4, TARSKI:def 1; :: thesis: verum

end;( 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

hence
( A <> {} & ( for B being Subset of Y holds
A6:
for m, n, o, p being set holds (m /\ n) /\ (o /\ p) = m /\ ((n /\ o) /\ p)

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 & N in PB ) and

A8: B = M /\ N by SETFAM_1:def 5;

consider S, T being set such that

A9: ( S in PA & T in PB ) and

A10: 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, A9, EQREL_1:def 4;

then A11: ( 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 A8, A10, A11, XBOOLE_0:def 7; :: thesis: verum

end;proof

let B be Subset of Y; :: thesis: ( not B in ia or A = B or A misses B )
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;(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

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 & N in PB ) and

A8: B = M /\ N by SETFAM_1:def 5;

consider S, T being set such that

A9: ( S in PA & T in PB ) and

A10: 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, A9, EQREL_1:def 4;

then A11: ( 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 A8, A10, A11, XBOOLE_0:def 7; :: thesis: verum

( not B in ia or A = B or A misses B ) ) ) by A4, TARSKI:def 1; :: thesis: verum