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

assume A1: x in X ; :: thesis: ex Z being set st
( x in Z & Z in Class EqR )
consider Z being set such that
A2: Z = Class EqR,x ;
Z in Class EqR by A1, A2, Def5;
hence ex Z being set st
( x in Z & Z in Class EqR ) by A1, A2, 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 consider x being set such that
A3: ( x in X & A = Class EqR,x ) by Def5;
thus A <> {} by A3, 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