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