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 = { x' where x' is Element of Y : S₂[x'] } as Subset of Y from DOMAIN_1:sch 7();
{C,D} \ {{} } is a_partition of Y

proof

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

proof

let a be set ; :: 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;

A2: 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 set ; :: 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 consider b being set such that
A3: ( a in b & b in {C,D} \ {{} } ) by TARSKI:def 4;
( a in C or a in D ) by A3, TARSKI:def 2;
hence a in Y ; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Y or a in union ({C,D} \ {{} }) )
assume a in Y ; :: thesis: a in union ({C,D} \ {{} })
then reconsider a = a as Element of Y ;
A4: ( f . a = TRUE or f . a = FALSE ) by TARSKI:def 2;
A5: ( C in {C,D} & D in {C,D} ) by TARSKI:def 2;

per cases ( a in C or a in D ) by A4;

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

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

end;

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

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

end;

end;

end;

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 ) ) ) )
assume A8: 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 ( A in {C,D} & 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 A9: B in {C,D} \ {{} } ; :: thesis: ( A = B or A misses B )
A10: C misses D

proof

now

given b being set such that A11: ( b in C & b in D ) ; :: thesis: contradiction

now

assume b in C ; :: thesis: not b in D
then consider x being Element of Y such that
A12: ( b = x & f . x = TRUE ) ;

now

assume b in D ; :: thesis: contradiction
then consider x' being Element of Y such that
A13: ( b = x' & f . x' = FALSE ) ;
thus contradiction by A12, A13; :: thesis: verum

end;

hence not b in D ; :: thesis: verum

end;

hence contradiction by A11; :: thesis: verum

end;

hence C misses D by XBOOLE_0:3; :: thesis: verum

end;

per cases ( ( A = C & B = C ) or ( A = D & B = D ) or ( A = C & B = D ) or ( A = D & B = C ) ) by A8, A9, 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 A10; :: thesis: verum

end;

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

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

end;

end;

end;

hence {C,D} \ {{} } is a_partition of Y by A1, A2, EQREL_1:def 6; :: thesis: verum

end;

hence {{ x where x is Element of Y : f . x = TRUE } ,{ x' where x' is Element of Y : f . x' = FALSE } } \ {{} } is a_partition of Y ; :: thesis: verum