let I be non empty set ; :: thesis: for M being ManySortedSet of I

for EqR being Equivalence_Relation of M holds EqR "\/" EqR = EqR

let M be ManySortedSet of I; :: thesis: for EqR being Equivalence_Relation of M holds EqR "\/" EqR = EqR

let EqR be Equivalence_Relation of M; :: thesis: EqR "\/" EqR = EqR

for EqR3 being Equivalence_Relation of M st EqR (\/) EqR c= EqR3 holds

EqR c= EqR3 ;

hence EqR "\/" EqR = EqR by Th6; :: thesis: verum

for EqR being Equivalence_Relation of M holds EqR "\/" EqR = EqR

let M be ManySortedSet of I; :: thesis: for EqR being Equivalence_Relation of M holds EqR "\/" EqR = EqR

let EqR be Equivalence_Relation of M; :: thesis: EqR "\/" EqR = EqR

for EqR3 being Equivalence_Relation of M st EqR (\/) EqR c= EqR3 holds

EqR c= EqR3 ;

hence EqR "\/" EqR = EqR by Th6; :: thesis: verum