defpred S₁[ set ] means f . $1 = TRUE ;
reconsider C = { x where x is Element of Y : S₁[x] } as Subset of Y from DOMAIN_1:sch 7();
defpred S₂[ set ] means f . $1 = FALSE ;
reconsider D = { x9 where x9 is Element of Y : S₂[x9] } as Subset of Y from DOMAIN_1:sch 7();
A1: union ({C,D} \ {{}}) = Y

thus union ({C,D} \ {{}}) c= Y :: according to XBOOLE_0:def 10 :: thesis:

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in union ({C,D} \ {{}}) ; :: thesis:
then ex b being set st
( a in b & b in {C,D} \ {{}} ) by TARSKI:def 4;
then ( a in C or a in D ) by TARSKI:def 2;
hence a in Y ; :: thesis:

end;

let a be object ; :: according to TARSKI:def 3 :: thesis:
A2: C in {C,D} by TARSKI:def 2;
assume a in Y ; :: thesis:
then reconsider a = a as Element of Y ;
A3: ( f . a = TRUE or f . a = FALSE ) by TARSKI:def 2;
A4: D in {C,D} by TARSKI:def 2;

per cases by A3;

suppose A5: a in C ; :: thesis:

then not C in {{}} by TARSKI:def 1;
then C in {C,D} \ {{}} by A2, XBOOLE_0:def 5;
hence a in union ({C,D} \ {{}}) by A5, TARSKI:def 4; :: thesis:

end;

suppose A6: a in D ; :: thesis:

then not D in {{}} by TARSKI:def 1;
then D in {C,D} \ {{}} by A4, XBOOLE_0:def 5;
hence a in union ({C,D} \ {{}}) by A6, TARSKI:def 4; :: thesis:

end;

end;

end;

A7: for A being Subset of Y st A in {C,D} \ {{}} holds
( A <> {} & ( for B being Subset of Y holds
( not B in {C,D} \ {{}} or A = B or A misses B ) ) )

let A be Subset of Y; :: thesis:

A8: now :: thesis:

given b being object such that A9: ( b in C & b in D ) ; :: thesis:

assume b in C ; :: thesis:
then A10: ex x being Element of Y st
( b = x & f . x = TRUE ) ;

assume b in D ; :: thesis:
then ex x9 being Element of Y st
( b = x9 & f . x9 = FALSE ) ;
hence contradiction by A10; :: thesis:

end;

hence not b in D ; :: thesis:

end;

hence contradiction by A9; :: thesis:

end;

assume A11: A in {C,D} \ {{}} ; :: thesis:
then not A in {{}} by XBOOLE_0:def 5;
hence A <> {} by TARSKI:def 1; :: thesis:
let B be Subset of Y; :: thesis:
assume A12: B in {C,D} \ {{}} ; :: thesis:

per cases by A11, A12, TARSKI:def 2;

suppose ( A = C & B = C ) ; :: thesis:

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

end;

suppose ( A = D & B = D ) ; :: thesis:

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

end;

suppose ( A = C & B = D ) ; :: thesis:

hence ( A = B or A misses B ) by A8, XBOOLE_0:3; :: thesis:

end;

suppose ( A = D & B = C ) ; :: thesis:

hence ( A = B or A misses B ) by A8, XBOOLE_0:3; :: thesis:

end;

end;

end;

{C,D} \ {{}} c= bool Y

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in {C,D} \ {{}} ; :: thesis:
then ( a = C or a = D ) by TARSKI:def 2;
hence a in bool Y ; :: thesis:

end;

hence { { x where x is Element of Y : f . x = TRUE } , { x9 where x9 is Element of Y : f . x9 = FALSE } } \ {{}} is a_partition of Y by A1, A7, EQREL_1:def 4; :: thesis: