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

E is a_partition of the carrier of XX

D \/ { {p} where p is Point of XX : not p in the carrier of X } c= bool the carrier of XX

proof

then reconsider E = D \/ { {p} where p is Point of XX : not p in the carrier of X } as Subset-Family of XX ;
let e be object ; :: 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

end;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 :: thesis: e in bool the carrier of XXend;

hence
e in bool the carrier of XX
; :: thesis: verumper 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;

end;

E is a_partition of the carrier of XX

proof

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 Th1, XBOOLE_1:45 ; :: according to EQREL_1:def 4 :: thesis: for b_{1} being Element of bool the carrier of XX holds

( not b_{1} in E or ( not b_{1} = {} & ( for b_{2} being Element of bool the carrier of XX holds

( not b_{2} in E or b_{1} = b_{2} or b_{1} misses b_{2} ) ) ) )

let A be Subset of XX; :: thesis: ( not A in E or ( not A = {} & ( for b_{1} being Element of bool the carrier of XX holds

( not b_{1} in E or A = b_{1} or A misses b_{1} ) ) ) )

assume A9: A in E ; :: thesis: ( not A = {} & ( for b_{1} being Element of bool the carrier of XX holds

( not b_{1} in E or A = b_{1} or A misses b_{1} ) ) )

_{1} being Element of bool the carrier of XX holds

( not b_{1} in E or A = b_{1} or A misses b_{1} )

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 )

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: verumnow :: thesis: for e being object holds

( ( 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 ) )

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

let e be object ; :: 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 )

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

given Z being set such that A4:
e in Z
and
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;( 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

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

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 Th1, XBOOLE_1:45 ; :: according to EQREL_1:def 4 :: thesis: for b

( not b

( not b

let A be Subset of XX; :: thesis: ( not A in E or ( not A = {} & ( for b

( not b

assume A9: A in E ; :: thesis: ( not A = {} & ( for b

( not b

now :: thesis: A <> {}

hence
A <> {}
; :: thesis: for bend;

( not b

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 :: thesis: ( A = B or A misses B )end;

hence
( A = B or A misses B )
; :: thesis: verumper 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;

end;

suppose A11:
A in D
; :: thesis: ( A = B or A misses B )

end;

now :: thesis: ( A = B or A misses B )

hence
( A = B or A misses B )
; :: thesis: verumend;

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;

end;( A = {p} & not p in the carrier of X ) ;

then A13: A misses the carrier of X by ZFMISC_1:50;

now :: thesis: ( A = B or A misses B )

hence
( A = B or A misses B )
; :: thesis: verumend;