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