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

per cases ( not F is empty or F is empty ) ;

suppose not F is empty ; :: thesis: meet |:F:| is MSCongruence of A

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)

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in F1 or q in the carrier of (EqRelLatt the Sorts of A) )
assume q in F1 ; :: thesis: q in the carrier of (EqRelLatt the Sorts of A)
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: verum

end;

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

now :: thesis: for o being OperSymbol of S
for a, b being Element of Args (o,A) st ( for n being Nat st n in dom a holds
[(a . n),(b . n)] in R0 . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . a),((Den (o,A)) . b)] in R0 . (the_result_sort_of o)

let o be OperSymbol of S; :: thesis: for a, b being Element of Args (o,A) st ( for n being Nat st n in dom a holds
[(a . n),(b . n)] in R0 . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . a),((Den (o,A)) . b)] in R0 . (the_result_sort_of o)
let a, b be Element of Args (o,A); :: thesis: ( ( for n being Nat st n in dom a holds
[(a . n),(b . n)] in R0 . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . a),((Den (o,A)) . b)] in R0 . (the_result_sort_of o) )
assume A4: for n being Nat st n in dom a holds
[(a . n),(b . n)] in R0 . ((the_arity_of o) /. n) ; :: thesis: [((Den (o,A)) . a),((Den (o,A)) . b)] in R0 . (the_result_sort_of o)
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 1;
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:14;

now :: thesis: for Y being set st Y in Q holds
[((Den (o,A)) . a),((Den (o,A)) . b)] in Y

let Y be set ; :: thesis: ( Y in Q implies [((Den (o,A)) . a),((Den (o,A)) . b)] in Y )
assume Y in Q ; :: thesis: [((Den (o,A)) . a),((Den (o,A)) . b)] in Y
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;

now :: thesis: for n being Nat st n in dom a holds
[(a . n),(b . n)] in s . ((the_arity_of o) /. n)

let n be Nat; :: thesis: ( n in dom a implies [(a . n),(b . n)] in s . ((the_arity_of o) /. n) )
assume A10: n in dom a ; :: thesis: [(a . n),(b . n)] in s . ((the_arity_of o) /. n)
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 1;
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:14;
then A13: s . ((the_arity_of o) /. n) in G by A9;
[(a . n),(b . n)] in Intersect G by A4, A10, A12;
then [(a . n),(b . n)] in meet G by A11, SETFAM_1:def 9;
hence [(a . n),(b . n)] in s . ((the_arity_of o) /. n) by A13, SETFAM_1:def 1; :: thesis: verum

end;

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

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 9; :: thesis: verum

end;

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

end;

suppose F is empty ; :: thesis: meet |:F:| is MSCongruence of A

then |:F:| = EmptyMS the carrier of S ;
then meet |:F:| = [| the Sorts of A, the Sorts of A|] by MSSUBFAM:41;
hence meet |:F:| is MSCongruence of A by MSUALG_5:18; :: thesis: verum

end;

end;