let X be set ; :: thesis: for EqR1 being Equivalence_Relation of X holds EqCl EqR1 = EqR1

let EqR1 be Equivalence_Relation of X; :: thesis: EqCl EqR1 = EqR1

for EqR2 being Equivalence_Relation of X st EqR1 c= EqR2 holds

EqR1 c= EqR2 ;

hence EqCl EqR1 = EqR1 by Def1; :: thesis: verum

let EqR1 be Equivalence_Relation of X; :: thesis: EqCl EqR1 = EqR1

for EqR2 being Equivalence_Relation of X st EqR1 c= EqR2 holds

EqR1 c= EqR2 ;

hence EqCl EqR1 = EqR1 by Def1; :: thesis: verum