let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S

for C1, C2 being MSCongruence of A holds C1 "\/" C2 is MSCongruence of A

let A be non-empty MSAlgebra over S; :: thesis: for C1, C2 being MSCongruence of A holds C1 "\/" C2 is MSCongruence of A

let C1, C2 be MSCongruence of A; :: thesis: C1 "\/" C2 is MSCongruence of A

reconsider C = C1 "\/" C2 as MSEquivalence_Relation-like ManySortedRelation of the Sorts of A ;

reconsider C = C as ManySortedRelation of A ;

reconsider C = C as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def 3;

for o being OperSymbol of S

for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds

[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds

[((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) by Th14;

hence C1 "\/" C2 is MSCongruence of A by MSUALG_4:def 4; :: thesis: verum

for C1, C2 being MSCongruence of A holds C1 "\/" C2 is MSCongruence of A

let A be non-empty MSAlgebra over S; :: thesis: for C1, C2 being MSCongruence of A holds C1 "\/" C2 is MSCongruence of A

let C1, C2 be MSCongruence of A; :: thesis: C1 "\/" C2 is MSCongruence of A

reconsider C = C1 "\/" C2 as MSEquivalence_Relation-like ManySortedRelation of the Sorts of A ;

reconsider C = C as ManySortedRelation of A ;

reconsider C = C as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def 3;

for o being OperSymbol of S

for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds

[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds

[((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) by Th14;

hence C1 "\/" C2 is MSCongruence of A by MSUALG_4:def 4; :: thesis: verum