begin
theorem Th1:
theorem Th2:
theorem
theorem
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
begin
theorem Th11:
:: deftheorem defines CongrCl MSUALG_8:def 1 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for E being Element of (EqRelLatt the Sorts of A) holds CongrCl E = "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ,(EqRelLatt the Sorts of A));
:: deftheorem defines CongrCl MSUALG_8:def 2 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for X being Subset of (EqRelLatt the Sorts of A) holds CongrCl X = "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ,(EqRelLatt the Sorts of A));
theorem
theorem
theorem
theorem
theorem Th16:
:: deftheorem Def3 defines EqRelSet MSUALG_8:def 3 :
for I being non empty set
for M being ManySortedSet of I
for i being Element of I
for X being Subset of (EqRelLatt M)
for b5 being Subset of (EqRelLatt (M . i)) holds
( b5 = EqRelSet (X,i) iff for x being set holds
( x in b5 iff ex Eq being Equivalence_Relation of M st
( x = Eq . i & Eq in X ) ) );
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20: