let X be set ; :: thesis: for EqR being Equivalence_Relation of X holds Class EqR is a_partition of X

let EqR be Equivalence_Relation of X; :: thesis: Class EqR is a_partition of X

( A <> {} & ( for B being Subset of X holds

( not B in Class EqR or A = B or A misses B ) ) )

let A be Subset of X; :: thesis: ( A in Class EqR implies ( A <> {} & ( for B being Subset of X holds

( not B in Class EqR or A = B or A misses B ) ) ) )

assume A in Class EqR ; :: thesis: ( A <> {} & ( for B being Subset of X holds

( not B in Class EqR or A = B or A misses B ) ) )

then A3: ex x being object st

( x in X & A = Class (EqR,x) ) by Def3;

hence A <> {} by Th20; :: thesis: for B being Subset of X holds

( not B in Class EqR or A = B or A misses B )

let B be Subset of X; :: thesis: ( not B in Class EqR or A = B or A misses B )

assume B in Class EqR ; :: thesis: ( A = B or A misses B )

then ex y being object st

( y in X & B = Class (EqR,y) ) by Def3;

hence ( A = B or A misses B ) by A3, Th24; :: thesis: verum

let EqR be Equivalence_Relation of X; :: thesis: Class EqR is a_partition of X

now :: thesis: for x being object holds

( x in X iff ex Z being set st

( x in Z & Z in Class EqR ) )

hence
union (Class EqR) = X
by TARSKI:def 4; :: according to EQREL_1:def 4 :: thesis: for A being Subset of X st A in Class EqR holds ( x in X iff ex Z being set st

( x in Z & Z in Class EqR ) )

let x be object ; :: thesis: ( x in X iff ex Z being set st

( x in Z & Z in Class EqR ) )

( x in Z & Z in Class EqR ) ) ; :: thesis: verum

end;( x in Z & Z in Class EqR ) )

now :: thesis: ( x in X implies ex Z being set st

( x in Z & Z in Class EqR ) )

hence
( x in X iff ex Z being set st ( x in Z & Z in Class EqR ) )

consider Z being set such that

A1: Z = Class (EqR,x) ;

assume A2: x in X ; :: thesis: ex Z being set st

( x in Z & Z in Class EqR )

then Z in Class EqR by A1, Def3;

hence ex Z being set st

( x in Z & Z in Class EqR ) by A2, A1, Th20; :: thesis: verum

end;A1: Z = Class (EqR,x) ;

assume A2: x in X ; :: thesis: ex Z being set st

( x in Z & Z in Class EqR )

then Z in Class EqR by A1, Def3;

hence ex Z being set st

( x in Z & Z in Class EqR ) by A2, A1, Th20; :: thesis: verum

( x in Z & Z in Class EqR ) ) ; :: thesis: verum

( A <> {} & ( for B being Subset of X holds

( not B in Class EqR or A = B or A misses B ) ) )

let A be Subset of X; :: thesis: ( A in Class EqR implies ( A <> {} & ( for B being Subset of X holds

( not B in Class EqR or A = B or A misses B ) ) ) )

assume A in Class EqR ; :: thesis: ( A <> {} & ( for B being Subset of X holds

( not B in Class EqR or A = B or A misses B ) ) )

then A3: ex x being object st

( x in X & A = Class (EqR,x) ) by Def3;

hence A <> {} by Th20; :: thesis: for B being Subset of X holds

( not B in Class EqR or A = B or A misses B )

let B be Subset of X; :: thesis: ( not B in Class EqR or A = B or A misses B )

assume B in Class EqR ; :: thesis: ( A = B or A misses B )

then ex y being object st

( y in X & B = Class (EqR,y) ) by Def3;

hence ( A = B or A misses B ) by A3, Th24; :: thesis: verum