let S be non empty non void ManySortedSign ; :: thesis:
let A be non-empty MSAlgebra of S; :: thesis:
let R be Subset of (CongrLatt A); :: thesis:
let F be SubsetFamily of [|the Sorts of A,the Sorts of A|]; :: thesis:
assume A1: R = F ; :: thesis:
set R0 = meet |:F:|;
set SF = the Sorts of A;
set I = the carrier of S;

per cases ;

suppose not F is empty ; :: thesis:

then reconsider F1 = F as non empty SubsetFamily of [|the Sorts of A,the Sorts of A|] ;
A2: F1 c= the carrier of (EqRelLatt the Sorts of A)

let q be set ; :: according to TARSKI:def 3 :: thesis:
assume q in F1 ; :: thesis:
then q is MSCongruence of A by A1, MSUALG_5:def 6;
hence q in the carrier of (EqRelLatt the Sorts of A) by MSUALG_5:def 5; :: thesis:

end;

then A3: meet |:F:| is MSEquivalence_Relation-like ManySortedRelation of the Sorts of A by MSUALG_7:9;
reconsider R0 = meet |:F:| as ManySortedRelation of A by A2, MSUALG_7:9;
R0 is MSEquivalence-like

let i be set ; :: according to MSUALG_4:def 3,MSUALG_4:def 5 :: thesis:
let R be Relation of (the Sorts of A . i); :: thesis:
assume ( i in the carrier of S & R0 . i = R ) ; :: thesis:
hence R is Element of bool [:(the Sorts of A . i),(the Sorts of A . i):] by A3, MSUALG_4:def 3; :: thesis:

end;

then reconsider R0 = R0 as MSEquivalence-like ManySortedRelation of A ;

let o be OperSymbol of S; :: thesis:
let a, b be Element of Args o,A; :: thesis:
assume A4: for n being Nat st n in dom a holds
[(a . n),(b . n)] in R0 . ((the_arity_of o) /. n) ; :: thesis:
set r = the_result_sort_of o;
consider Q being Subset-Family of ([|the Sorts of A,the Sorts of A|] . (the_result_sort_of o)) such that
A5: Q = |:F1:| . (the_result_sort_of o) and
A6: R0 . (the_result_sort_of o) = Intersect Q by MSSUBFAM:def 2;
A7: Q = { (s . (the_result_sort_of o)) where s is Element of Bool [|the Sorts of A,the Sorts of A|] : s in F1 } by A5, CLOSURE2:15;

let Y be set ; :: thesis:
assume Y in Q ; :: thesis:
then consider s being Element of Bool [|the Sorts of A,the Sorts of A|] such that
A8: Y = s . (the_result_sort_of o) and
A9: s in F1 by A7;
reconsider s = s as MSCongruence of A by A1, A9, MSUALG_5:def 6;

let n be Nat; :: thesis:
assume A10: n in dom a ; :: thesis:
set t = (the_arity_of o) /. n;
consider G being Subset-Family of ([|the Sorts of A,the Sorts of A|] . ((the_arity_of o) /. n)) such that
A11: G = |:F1:| . ((the_arity_of o) /. n) and
A12: R0 . ((the_arity_of o) /. n) = Intersect G by MSSUBFAM:def 2;
[(a . n),(b . n)] in Intersect G by A4, A10, A12;
then A13: [(a . n),(b . n)] in meet G by A11, SETFAM_1:def 10;
G = { (j . ((the_arity_of o) /. n)) where j is Element of Bool [|the Sorts of A,the Sorts of A|] : j in F1 } by A11, CLOSURE2:15;
then s . ((the_arity_of o) /. n) in G by A9;
hence [(a . n),(b . n)] in s . ((the_arity_of o) /. n) by A13, SETFAM_1:def 1; :: thesis:

end;

hence [((Den o,A) . a),((Den o,A) . b)] in Y by A8, MSUALG_4:def 6; :: thesis:

end;

then [((Den o,A) . a),((Den o,A) . b)] in meet Q by A5, SETFAM_1:def 1;
hence [((Den o,A) . a),((Den o,A) . b)] in R0 . (the_result_sort_of o) by A5, A6, SETFAM_1:def 10; :: thesis:

end;

hence meet |:F:| is MSCongruence of A by MSUALG_4:def 6; :: thesis:

end;

suppose F is empty ; :: thesis:

then |:F:| = [0] the carrier of S by CLOSURE2:def 4;
then meet |:F:| = [|the Sorts of A,the Sorts of A|] by MSSUBFAM:41;
hence meet |:F:| is MSCongruence of A by MSUALG_5:20; :: thesis:

end;