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

proof

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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union ({C,D} \ {{}}) or a in Y )
assume a in union ({C,D} \ {{}}) ; :: thesis: a in Y
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: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Y or a in union ({C,D} \ {{}}) )
A2: C in {C,D} by TARSKI:def 2;
assume a in Y ; :: thesis: a in union ({C,D} \ {{}})
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 ( a in C or a in D ) by A3;

suppose A5: a in C ; :: thesis: a in union ({C,D} \ {{}})

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: verum

end;

suppose A6: a in D ; :: thesis: a in union ({C,D} \ {{}})

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: verum

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

proof

let A be Subset of Y; :: thesis: ( A in {C,D} \ {{}} implies ( A <> {} & ( for B being Subset of Y holds
( not B in {C,D} \ {{}} or A = B or A misses B ) ) ) )

A8: now :: thesis: for b being object holds
( not b in C or not b in D )

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

now :: thesis: ( b in C implies not b in D )

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

now :: thesis: not b in D

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

end;

hence not b in D ; :: thesis: verum

end;

hence contradiction by A9; :: thesis: verum

end;

assume A11: A in {C,D} \ {{}} ; :: thesis: ( A <> {} & ( for B being Subset of Y holds
( not B in {C,D} \ {{}} or A = B or A misses B ) ) )
then not A in {{}} by XBOOLE_0:def 5;
hence A <> {} by TARSKI:def 1; :: thesis: for B being Subset of Y holds
( not B in {C,D} \ {{}} or A = B or A misses B )
let B be Subset of Y; :: thesis: ( not B in {C,D} \ {{}} or A = B or A misses B )
assume A12: B in {C,D} \ {{}} ; :: thesis: ( A = B or A misses B )

per cases ( ( A = C & B = C ) or ( A = D & B = D ) or ( A = C & B = D ) or ( A = D & B = C ) ) by A11, A12, TARSKI:def 2;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

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

proof

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

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: verum