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

now

let x be set ; :: thesis: ( x in X iff ex Z being set st
( x in Z & Z in Class EqR ) )

now

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, Def5;
hence ex Z being set st
( x in Z & Z in Class EqR ) by A2, A1, Th28; :: thesis: verum

end;

hence ( x in X iff ex Z being set st
( x in Z & Z in Class EqR ) ) ; :: thesis: verum

end;

hence union (Class EqR) = X by TARSKI:def 4; :: according to EQREL_1:def 6 :: thesis: for A being Subset of X st A in Class EqR holds
( 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 set st
( x in X & A = Class (EqR,x) ) by Def5;
hence A <> {} by Th28; :: 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 set st
( y in X & B = Class (EqR,y) ) by Def5;
hence ( A = B or A misses B ) by A3, Th32; :: thesis: verum