let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for C1, C2 being MSCongruence of A holds C1 "\/" C2 is MSCongruence of A
let A be non-empty MSAlgebra of 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 5;
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 Th16;
hence C1 "\/" C2 is MSCongruence of A by MSUALG_4:def 6; :: thesis: verum