let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for B being Subset of (CongrLatt A) holds "/\" B,(EqRelLatt the Sorts of A) is MSCongruence of A
let A be non-empty MSAlgebra of S; :: thesis: for B being Subset of (CongrLatt A) holds "/\" B,(EqRelLatt the Sorts of A) is MSCongruence of A
set M = the Sorts of A;
set E = EqRelLatt the Sorts of A;
set C = CongrLatt A;
let B be Subset of (CongrLatt A); :: thesis: "/\" B,(EqRelLatt the Sorts of A) is MSCongruence of A
the carrier of (CongrLatt A) c= the carrier of (EqRelLatt the Sorts of A) by NAT_LAT:def 16;
then reconsider B1 = B as Subset of (EqRelLatt the Sorts of A) by XBOOLE_1:1;
reconsider B1 = B1 as SubsetFamily of [|the Sorts of A,the Sorts of A|] by MSUALG_7:6;
set d' = "/\" B,(EqRelLatt the Sorts of A);
reconsider d = "/\" B,(EqRelLatt the Sorts of A) as Equivalence_Relation of the Sorts of A by MSUALG_5:def 5;
reconsider d = d as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def 5;

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

suppose B is empty ; :: thesis: "/\" B,(EqRelLatt the Sorts of A) is MSCongruence of A

then reconsider B' = B as empty Subset of (CongrLatt A) ;
for q being Element of (EqRelLatt the Sorts of A) st q in B' holds
Top (EqRelLatt the Sorts of A) [= q ;
then A1: Top (EqRelLatt the Sorts of A) is_less_than B by LATTICE3:def 16;
for b being Element of (EqRelLatt the Sorts of A) st b is_less_than B holds
b [= Top (EqRelLatt the Sorts of A) by LATTICES:45;
then "/\" B,(EqRelLatt the Sorts of A) = Top (EqRelLatt the Sorts of A) by A1, LATTICE3:34
.= [|the Sorts of A,the Sorts of A|] by MSUALG_7:5 ;
hence "/\" B,(EqRelLatt the Sorts of A) is MSCongruence of A by MSUALG_5:20; :: thesis: verum

end;

suppose A2: not B is empty ; :: thesis: "/\" B,(EqRelLatt the Sorts of A) is MSCongruence of A

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 d . ((the_arity_of o) /. n) ) holds
[((Den o,A) . x),((Den o,A) . y)] in d . (the_result_sort_of o)

proof

let o be OperSymbol of S; :: thesis: 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 d . ((the_arity_of o) /. n) ) holds
[((Den o,A) . x),((Den o,A) . y)] in d . (the_result_sort_of o)
let x, y be Element of Args o,A; :: thesis: ( ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in d . ((the_arity_of o) /. n) ) implies [((Den o,A) . x),((Den o,A) . y)] in d . (the_result_sort_of o) )
assume A3: for n being Nat st n in dom x holds
[(x . n),(y . n)] in d . ((the_arity_of o) /. n) ; :: thesis: [((Den o,A) . x),((Den o,A) . y)] in d . (the_result_sort_of o)
reconsider m = meet |:B1:| as Equivalence_Relation of the Sorts of A by A2, MSUALG_7:9;

A4: now

let q be MSCongruence of A; :: thesis: ( q in B implies [((Den o,A) . x),((Den o,A) . y)] in q . (the_result_sort_of o) )
assume A5: q in B ; :: thesis: [((Den o,A) . x),((Den o,A) . y)] in q . (the_result_sort_of o)

now

let n be Nat; :: thesis: ( n in dom x implies [(x . n),(y . n)] in q . ((the_arity_of o) /. n) )
assume A6: n in dom x ; :: thesis: [(x . n),(y . n)] in q . ((the_arity_of o) /. n)
m c= q by A5, MSUALG_7:8;
then A7: m . ((the_arity_of o) /. n) c= q . ((the_arity_of o) /. n) by PBOOLE:def 5;
[(x . n),(y . n)] in d . ((the_arity_of o) /. n) by A3, A6;
then [(x . n),(y . n)] in m . ((the_arity_of o) /. n) by A2, MSUALG_7:11;
hence [(x . n),(y . n)] in q . ((the_arity_of o) /. n) by A7; :: thesis: verum

end;

hence [((Den o,A) . x),((Den o,A) . y)] in q . (the_result_sort_of o) by MSUALG_4:def 6; :: thesis: verum

end;

consider Q being Subset-Family of ([|the Sorts of A,the Sorts of A|] . (the_result_sort_of o)) such that
A8: ( Q = |:B1:| . (the_result_sort_of o) & m . (the_result_sort_of o) = Intersect Q ) by MSSUBFAM:def 2;
reconsider B1' = B1 as non empty SubsetFamily of [|the Sorts of A,the Sorts of A|] by A2;
|:B1':| is non-empty ;
then A9: Q <> {} by A8;
A10: |:B1:| . (the_result_sort_of o) = { (x1 . (the_result_sort_of o)) where x1 is Element of Bool [|the Sorts of A,the Sorts of A|] : x1 in B } by A2, CLOSURE2:15;

now

let Y be set ; :: thesis: ( Y in |:B1:| . (the_result_sort_of o) implies [((Den o,A) . x),((Den o,A) . y)] in Y )
assume Y in |:B1:| . (the_result_sort_of o) ; :: thesis: [((Den o,A) . x),((Den o,A) . y)] in Y
then consider z being Element of Bool [|the Sorts of A,the Sorts of A|] such that
A11: ( Y = z . (the_result_sort_of o) & z in B ) by A10;
reconsider z' = z as MSCongruence of A by A11, MSUALG_5:def 6;
[((Den o,A) . x),((Den o,A) . y)] in z' . (the_result_sort_of o) by A4, A11;
hence [((Den o,A) . x),((Den o,A) . y)] in Y by A11; :: thesis: verum

end;

then [((Den o,A) . x),((Den o,A) . y)] in meet (|:B1:| . (the_result_sort_of o)) by A8, A9, SETFAM_1:def 1;
then [((Den o,A) . x),((Den o,A) . y)] in m . (the_result_sort_of o) by A8, A9, SETFAM_1:def 10;
hence [((Den o,A) . x),((Den o,A) . y)] in d . (the_result_sort_of o) by A2, MSUALG_7:11; :: thesis: verum

end;

hence "/\" B,(EqRelLatt the Sorts of A) is MSCongruence of A by MSUALG_4:def 6; :: thesis: verum

end;

end;