{} 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
proof
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;
then reconsider a = INTERSECTION (PA,PB) as Subset-Family of Y by TARSKI:def 3;
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
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 & 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;
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 4; :: thesis: verum