set E = D \/ { {p} where p is Point of XX : not p in the carrier of X } ;
D \/ { {p} where p is Point of XX : not p in the carrier of X } c= bool the carrier of XX
proof
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in D \/ { {p} where p is Point of XX : not p in the carrier of X } or e in bool the carrier of XX )
assume A1: e in D \/ { {p} where p is Point of XX : not p in the carrier of X } ; :: thesis: e in bool the carrier of XX
now
per cases ( e in D or e in { {p} where p is Point of XX : not p in the carrier of X } ) by A1, XBOOLE_0:def 3;
suppose A2: e in D ; :: thesis: e in bool the carrier of XX
bool the carrier of X c= bool the carrier of XX by Th35, ZFMISC_1:67;
hence e in bool the carrier of XX by A2, TARSKI:def 3; :: thesis: verum
end;
suppose e in { {p} where p is Point of XX : not p in the carrier of X } ; :: thesis: e in bool the carrier of XX
then ex p being Point of XX st
( e = {p} & not p in the carrier of X ) ;
hence e in bool the carrier of XX ; :: thesis: verum
end;
end;
end;
hence e in bool the carrier of XX ; :: thesis: verum
end;
then reconsider E = D \/ { {p} where p is Point of XX : not p in the carrier of X } as Subset-Family of XX ;
E is a_partition of the carrier of XX
proof
now
let e be set ; :: thesis: ( ( e in the carrier of XX \ the carrier of X implies ex Z being set st
( e in Z & Z in { {p} where p is Point of XX : not p in the carrier of X } ) ) & ( ex Z being set st
( e in Z & Z in { {p} where p is Point of XX : not p in the carrier of X } ) implies e in the carrier of XX \ the carrier of X ) )
thus ( e in the carrier of XX \ the carrier of X implies ex Z being set st
( e in Z & Z in { {p} where p is Point of XX : not p in the carrier of X } ) ) :: thesis: ( ex Z being set st
( e in Z & Z in { {p} where p is Point of XX : not p in the carrier of X } ) implies e in the carrier of XX \ the carrier of X )
proof
assume A3: e in the carrier of XX \ the carrier of X ; :: thesis: ex Z being set st
( e in Z & Z in { {p} where p is Point of XX : not p in the carrier of X } )
take {e} ; :: thesis: ( e in {e} & {e} in { {p} where p is Point of XX : not p in the carrier of X } )
thus e in {e} by TARSKI:def 1; :: thesis: {e} in { {p} where p is Point of XX : not p in the carrier of X }
not e in the carrier of X by A3, XBOOLE_0:def 5;
hence {e} in { {p} where p is Point of XX : not p in the carrier of X } by A3; :: thesis: verum
end;
given Z being set such that A4: e in Z and
A5: Z in { {p} where p is Point of XX : not p in the carrier of X } ; :: thesis: e in the carrier of XX \ the carrier of X
consider p being Point of XX such that
A6: Z = {p} and
A7: not p in the carrier of X by A5;
e = p by A4, A6, TARSKI:def 1;
hence e in the carrier of XX \ the carrier of X by A7, XBOOLE_0:def 5; :: thesis: verum
end;
then A8: union { {p} where p is Point of XX : not p in the carrier of X } = the carrier of XX \ the carrier of X by TARSKI:def 4;
thus union E = (union D) \/ (union { {p} where p is Point of XX : not p in the carrier of X } ) by ZFMISC_1:78
.= the carrier of X \/ ( the carrier of XX \ the carrier of X) by A8, EQREL_1:def 4
.= the carrier of XX by Th35, XBOOLE_1:45 ; :: according to EQREL_1:def 4 :: thesis: for b1 being Element of bool the carrier of XX holds
( not b1 in E or ( not b1 = {} & ( for b2 being Element of bool the carrier of XX holds
( not b2 in E or b1 = b2 or b1 misses b2 ) ) ) )
let A be Subset of XX; :: thesis: ( not A in E or ( not A = {} & ( for b1 being Element of bool the carrier of XX holds
( not b1 in E or A = b1 or A misses b1 ) ) ) )
assume A9: A in E ; :: thesis: ( not A = {} & ( for b1 being Element of bool the carrier of XX holds
( not b1 in E or A = b1 or A misses b1 ) ) )
now
per cases ( A in D or A in { {p} where p is Point of XX : not p in the carrier of X } ) by A9, XBOOLE_0:def 3;
suppose A in { {p} where p is Point of XX : not p in the carrier of X } ; :: thesis: A <> {}
then ex p being Point of XX st
( A = {p} & not p in the carrier of X ) ;
hence A <> {} ; :: thesis: verum
end;
end;
end;
hence A <> {} ; :: thesis: for b1 being Element of bool the carrier of XX holds
( not b1 in E or A = b1 or A misses b1 )
let B be Subset of XX; :: thesis: ( not B in E or A = B or A misses B )
assume A10: B in E ; :: thesis: ( A = B or A misses B )
now
per cases ( A in D or A in { {p} where p is Point of XX : not p in the carrier of X } ) by A9, XBOOLE_0:def 3;
suppose A11: A in D ; :: thesis: ( A = B or A misses B )
now
per cases ( B in D or B in { {p} where p is Point of XX : not p in the carrier of X } ) by A10, XBOOLE_0:def 3;
suppose B in D ; :: thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by A11, EQREL_1:def 4; :: thesis: verum
end;
suppose B in { {p} where p is Point of XX : not p in the carrier of X } ; :: thesis: ( A = B or A misses B )
then ex p being Point of XX st
( B = {p} & not p in the carrier of X ) ;
then B misses the carrier of X by ZFMISC_1:50;
hence ( A = B or A misses B ) by A11, XBOOLE_1:63; :: thesis: verum
end;
end;
end;
hence ( A = B or A misses B ) ; :: thesis: verum
end;
suppose A in { {p} where p is Point of XX : not p in the carrier of X } ; :: thesis: ( A = B or A misses B )
then A12: ex p being Point of XX st
( A = {p} & not p in the carrier of X ) ;
then A13: A misses the carrier of X by ZFMISC_1:50;
now
per cases ( B in D or B in { {p} where p is Point of XX : not p in the carrier of X } ) by A10, XBOOLE_0:def 3;
suppose B in D ; :: thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by A13, XBOOLE_1:63; :: thesis: verum
end;
suppose B in { {p} where p is Point of XX : not p in the carrier of X } ; :: thesis: ( A = B or A misses B )
then ex p being Point of XX st
( B = {p} & not p in the carrier of X ) ;
hence ( A = B or A misses B ) by A12, ZFMISC_1:11; :: thesis: verum
end;
end;
end;
hence ( A = B or A misses B ) ; :: thesis: verum
end;
end;
end;
hence ( A = B or A misses B ) ; :: thesis: verum
end;
hence D \/ { {p} where p is Point of XX : not p in the carrier of X } is non empty a_partition of the carrier of XX ; :: thesis: verum