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 :: thesis: for x being object 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 ) )
now :: thesis: ( x in X implies 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;
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 4 :: 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 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