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