:: MSUALG_5  semantic presentation begin  













definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "R" be   ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")); func  :::"EqCl"::: "R" ->   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" "X" means :: MSUALG_5:def 1 (Bool  "("  (Bool "R"  ($#r1_relset_1 :::"c="::: )  it) & (Bool  "("   "for" (Set (Var "EqR2")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" "X"  "st" (Bool (Bool "R"  ($#r1_relset_1 :::"c="::: )  (Set (Var "EqR2")))) "holds"  (Bool it  ($#r1_relset_1 :::"c="::: )  (Set (Var "EqR2")))  ")" )  ")" ); end; 






:: deftheorem    defines :::"EqCl"::: MSUALG_5:def 1 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_msualg_5 :::"EqCl"::: )  (Set (Var "R")))) "iff" (Bool  "("  (Bool (Set (Var "R"))  ($#r1_relset_1 :::"c="::: )  (Set (Var "b3"))) & (Bool  "("   "for" (Set (Var "EqR2")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "R"))  ($#r1_relset_1 :::"c="::: )  (Set (Var "EqR2")))) "holds"  (Bool (Set (Var "b3"))  ($#r1_relset_1 :::"c="::: )  (Set (Var "EqR2")))  ")" )  ")" )  ")" )))); 
 
theorem :: MSUALG_5:1 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "EqR1")) "," (Set (Var "EqR2")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "EqR1"))  ($#k5_eqrel_1 :::""\/""::: )  (Set (Var "EqR2")))  ($#r2_relset_1 :::"="::: )  (Set   ($#k1_msualg_5 :::"EqCl"::: )  (Set  "(" (Set (Var "EqR1"))  ($#k3_eqrel_1 :::"\/"::: )  (Set (Var "EqR2")) ")" ))))) ; 
 
theorem :: MSUALG_5:2 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "EqR1")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k1_msualg_5 :::"EqCl"::: )  (Set (Var "EqR1")))  ($#r2_relset_1 :::"="::: )  (Set (Var "EqR1"))))) ; 
 begin  definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"EqRelLatt"::: "X" ->   ($#v3_lattices :::"strict"::: )    ($#l3_lattices :::"Lattice":::) means :: MSUALG_5:def 2 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )   "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Relation":::) "of" "X" "," "X" : (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" "X")  "}"  ) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" "X" "holds"   (Bool  "("  (Bool (Set (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" it)  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k4_eqrel_1 :::"/\"::: )  (Set (Var "y")))) & (Bool (Set (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" it)  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_eqrel_1 :::""\/""::: )  (Set (Var "y"))))  ")" )  ")" )  ")" ); end; 





:: deftheorem    defines :::"EqRelLatt"::: MSUALG_5:def 2 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#v3_lattices :::"strict"::: )    ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_msualg_5 :::"EqRelLatt"::: )  (Set (Var "X")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "X")) : (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")))  "}"  ) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "b2")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k4_eqrel_1 :::"/\"::: )  (Set (Var "y")))) & (Bool (Set (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "b2")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_eqrel_1 :::""\/""::: )  (Set (Var "y"))))  ")" )  ")" )  ")" )  ")" ))); 
 begin  registrationlet "I" be    ($#m1_hidden :::"set"::: )  ; let "M" be   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   "I"  ($#v4_relat_1 :::"-defined"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_partfun1 :::"total"::: )   bbbadV2_FUNCOP_1()   ($#v1_msualg_4 :::"MSEquivalence_Relation-like"::: )    for    ($#m1_msualg_4 :::"ManySortedRelation"::: )   "of" "M" "," "M"; 
end; definitionlet "I" be    ($#m1_hidden :::"set"::: )  ; let "M" be   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); mode Equivalence_Relation of "M" is   ($#v1_msualg_4 :::"MSEquivalence_Relation-like"::: )    ($#m1_msualg_4 :::"ManySortedRelation":::) "of" "M"; end; 












definitionlet "I" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "M" be   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "R" be   ($#m1_msualg_4 :::"ManySortedRelation":::) "of" (Set (Const "M")); func  :::"EqCl"::: "R" ->   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" "M" means :: MSUALG_5:def 3 (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "I" "holds"  (Bool (Set it  ($#k1_msualg_4 :::"."::: )  (Set (Var "i")))  ($#r2_relset_1 :::"="::: )  (Set   ($#k1_msualg_5 :::"EqCl"::: )  (Set  "(" "R"  ($#k1_msualg_4 :::"."::: )  (Set (Var "i")) ")" )))); end; 







:: deftheorem    defines :::"EqCl"::: MSUALG_5:def 3 :  (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "R")) "being"   ($#m1_msualg_4 :::"ManySortedRelation":::) "of" (Set (Var "M"))  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_msualg_5 :::"EqCl"::: )  (Set (Var "R")))) "iff" (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_msualg_4 :::"."::: )  (Set (Var "i")))  ($#r2_relset_1 :::"="::: )  (Set   ($#k1_msualg_5 :::"EqCl"::: )  (Set  "(" (Set (Var "R"))  ($#k1_msualg_4 :::"."::: )  (Set (Var "i")) ")" ))))  ")" ))))); 
 
theorem :: MSUALG_5:3 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "EqR")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M")) "holds"  (Bool (Set   ($#k3_msualg_5 :::"EqCl"::: )  (Set (Var "EqR")))  ($#r8_pboole :::"="::: )  (Set (Var "EqR")))))) ; 
 begin  definitionlet "I" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "M" be   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "EqR1", "EqR2" be   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Const "M")); func "EqR1" :::""\/""::: "EqR2" ->   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" "M" means :: MSUALG_5:def 4 (Bool  "ex" (Set (Var "EqR3")) "being"   ($#m1_msualg_4 :::"ManySortedRelation":::) "of" "M" "st"  (Bool  "("  (Bool (Set (Var "EqR3"))  ($#r8_pboole :::"="::: )  (Set "EqR1"  ($#k2_pboole :::"\/"::: )  "EqR2")) & (Bool it  ($#r8_pboole :::"="::: )  (Set   ($#k3_msualg_5 :::"EqCl"::: )  (Set (Var "EqR3"))))  ")" )); commutativity  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "EqR1")) "," (Set (Var "EqR2")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Const "M"))  "st" (Bool (Bool  "ex" (Set (Var "EqR3")) "being"   ($#m1_msualg_4 :::"ManySortedRelation":::) "of" (Set (Const "M")) "st"  (Bool  "("  (Bool (Set (Var "EqR3"))  ($#r8_pboole :::"="::: )  (Set (Set (Var "EqR1"))  ($#k2_pboole :::"\/"::: )  (Set (Var "EqR2")))) & (Bool (Set (Var "b1"))  ($#r8_pboole :::"="::: )  (Set   ($#k3_msualg_5 :::"EqCl"::: )  (Set (Var "EqR3"))))  ")" ))) "holds"  (Bool  "ex" (Set (Var "EqR3")) "being"   ($#m1_msualg_4 :::"ManySortedRelation":::) "of" (Set (Const "M")) "st"  (Bool  "("  (Bool (Set (Var "EqR3"))  ($#r8_pboole :::"="::: )  (Set (Set (Var "EqR2"))  ($#k2_pboole :::"\/"::: )  (Set (Var "EqR1")))) & (Bool (Set (Var "b1"))  ($#r8_pboole :::"="::: )  (Set   ($#k3_msualg_5 :::"EqCl"::: )  (Set (Var "EqR3"))))  ")" )))
 ; end; 








:: deftheorem    defines :::""\/""::: MSUALG_5:def 4 :  (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "EqR1")) "," (Set (Var "EqR2")) "," (Set (Var "b5")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "EqR1"))  ($#k4_msualg_5 :::""\/""::: )  (Set (Var "EqR2")))) "iff" (Bool  "ex" (Set (Var "EqR3")) "being"   ($#m1_msualg_4 :::"ManySortedRelation":::) "of" (Set (Var "M")) "st"  (Bool  "("  (Bool (Set (Var "EqR3"))  ($#r8_pboole :::"="::: )  (Set (Set (Var "EqR1"))  ($#k2_pboole :::"\/"::: )  (Set (Var "EqR2")))) & (Bool (Set (Var "b5"))  ($#r8_pboole :::"="::: )  (Set   ($#k3_msualg_5 :::"EqCl"::: )  (Set (Var "EqR3"))))  ")" ))  ")" )))); 
 
theorem :: MSUALG_5:4 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "EqR1")) "," (Set (Var "EqR2")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M")) "holds"  (Bool (Set (Set (Var "EqR1"))  ($#k2_pboole :::"\/"::: )  (Set (Var "EqR2")))  ($#r2_pboole :::"c="::: )  (Set (Set (Var "EqR1"))  ($#k4_msualg_5 :::""\/""::: )  (Set (Var "EqR2"))))))) ; 
 
theorem :: MSUALG_5:5 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "EqR1")) "," (Set (Var "EqR2")) "," (Set (Var "EqR")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Set (Var "EqR1"))  ($#k2_pboole :::"\/"::: )  (Set (Var "EqR2")))  ($#r2_pboole :::"c="::: )  (Set (Var "EqR")))) "holds"  (Bool (Set (Set (Var "EqR1"))  ($#k4_msualg_5 :::""\/""::: )  (Set (Var "EqR2")))  ($#r2_pboole :::"c="::: )  (Set (Var "EqR")))))) ; 
 
theorem :: MSUALG_5:6 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "EqR1")) "," (Set (Var "EqR2")) "," (Set (Var "EqR3")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Set (Var "EqR1"))  ($#k2_pboole :::"\/"::: )  (Set (Var "EqR2")))  ($#r2_pboole :::"c="::: )  (Set (Var "EqR3"))) & (Bool  "("   "for" (Set (Var "EqR")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Set (Var "EqR1"))  ($#k2_pboole :::"\/"::: )  (Set (Var "EqR2")))  ($#r2_pboole :::"c="::: )  (Set (Var "EqR")))) "holds"  (Bool (Set (Var "EqR3"))  ($#r2_pboole :::"c="::: )  (Set (Var "EqR")))  ")" )) "holds"  (Bool (Set (Var "EqR3"))  ($#r8_pboole :::"="::: )  (Set (Set (Var "EqR1"))  ($#k4_msualg_5 :::""\/""::: )  (Set (Var "EqR2"))))))) ; 
 
theorem :: MSUALG_5:7 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "EqR")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M")) "holds"  (Bool (Set (Set (Var "EqR"))  ($#k4_msualg_5 :::""\/""::: )  (Set (Var "EqR")))  ($#r8_pboole :::"="::: )  (Set (Var "EqR")))))) ; 
 
theorem :: MSUALG_5:8 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "EqR1")) "," (Set (Var "EqR2")) "," (Set (Var "EqR3")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M")) "holds"  (Bool (Set (Set  "(" (Set (Var "EqR1"))  ($#k4_msualg_5 :::""\/""::: )  (Set (Var "EqR2")) ")" )  ($#k4_msualg_5 :::""\/""::: )  (Set (Var "EqR3")))  ($#r8_pboole :::"="::: )  (Set (Set (Var "EqR1"))  ($#k4_msualg_5 :::""\/""::: )  (Set  "(" (Set (Var "EqR2"))  ($#k4_msualg_5 :::""\/""::: )  (Set (Var "EqR3")) ")" )))))) ; 
 
theorem :: MSUALG_5:9 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "EqR1")) "," (Set (Var "EqR2")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M")) "holds"  (Bool (Set (Set (Var "EqR1"))  ($#k3_pboole :::"/\"::: )  (Set  "(" (Set (Var "EqR1"))  ($#k4_msualg_5 :::""\/""::: )  (Set (Var "EqR2")) ")" ))  ($#r8_pboole :::"="::: )  (Set (Var "EqR1")))))) ; 
 
theorem :: MSUALG_5:10 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "EqR1")) "," (Set (Var "EqR2")) "," (Set (Var "EqR")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Var "EqR"))  ($#r8_pboole :::"="::: )  (Set (Set (Var "EqR1"))  ($#k3_pboole :::"/\"::: )  (Set (Var "EqR2"))))) "holds"  (Bool (Set (Set (Var "EqR1"))  ($#k4_msualg_5 :::""\/""::: )  (Set (Var "EqR")))  ($#r8_pboole :::"="::: )  (Set (Var "EqR1")))))) ; 
 
theorem :: MSUALG_5:11 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "EqR1")) "," (Set (Var "EqR2")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M")) "holds"  (Bool (Set (Set (Var "EqR1"))  ($#k3_pboole :::"/\"::: )  (Set (Var "EqR2"))) "is"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M")))))) ; 
 definitionlet "I" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "M" be   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); func  :::"EqRelLatt"::: "M" ->   ($#v3_lattices :::"strict"::: )    ($#l3_lattices :::"Lattice":::) means :: MSUALG_5:def 5 (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)) "iff" (Bool (Set (Var "x")) "is"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" "M")  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" "M" "holds"   (Bool  "("  (Bool (Set (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" it)  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k3_pboole :::"/\"::: )  (Set (Var "y")))) & (Bool (Set (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" it)  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k4_msualg_5 :::""\/""::: )  (Set (Var "y"))))  ")" )  ")" )  ")" ); end; 






:: deftheorem    defines :::"EqRelLatt"::: MSUALG_5:def 5 :  (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "b3")) "being"   ($#v3_lattices :::"strict"::: )    ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set (Var "M")))) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))) "iff" (Bool (Set (Var "x")) "is"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M")))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "b3")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k3_pboole :::"/\"::: )  (Set (Var "y")))) & (Bool (Set (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "b3")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k4_msualg_5 :::""\/""::: )  (Set (Var "y"))))  ")" )  ")" )  ")" )  ")" )))); 
 begin  registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "A" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); 
cluster   ($#v2_msualg_4 :::"MSEquivalence-like"::: )    ->   ($#v1_msualg_4 :::"MSEquivalence_Relation-like"::: )    for    ($#m1_msualg_4 :::"ManySortedRelation"::: )   "of" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "A") "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "A"); 
end; 






theorem :: MSUALG_5:12 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"   ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a1")) "," (Set (Var "b1")) "being"   ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Set  "(" (Set (Var "C1"))  ($#k2_msualg_4 :::"."::: )  (Set  "(" (Set  "("  ($#k1_msualg_1 :::"the_arity_of"::: )  (Set (Var "o")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "a1")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k3_eqrel_1 :::"\/"::: )  (Set  "(" (Set (Var "C2"))  ($#k2_msualg_4 :::"."::: )  (Set  "(" (Set  "("  ($#k1_msualg_1 :::"the_arity_of"::: )  (Set (Var "o")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "a1")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )))) "holds"  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_msualg_1 :::"Args"::: )   "(" (Set (Var "o")) "," (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a1"))  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x1")) ($#k9_finseq_1 :::"*>"::: ) ) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set (Var "b1")))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a1"))  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "y1")) ($#k9_finseq_1 :::"*>"::: ) ) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set (Var "b1"))))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set  "("  ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ) "," (Set  "(" (Set  "("  ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Set  "(" (Set (Var "C1"))  ($#k2_msualg_4 :::"."::: )  (Set  "("  ($#k2_msualg_1 :::"the_result_sort_of"::: )  (Set (Var "o")) ")" ) ")" )  ($#k3_eqrel_1 :::"\/"::: )  (Set  "(" (Set (Var "C2"))  ($#k2_msualg_4 :::"."::: )  (Set  "("  ($#k2_msualg_1 :::"the_result_sort_of"::: )  (Set (Var "o")) ")" ) ")" )))))))))) ; 
 
theorem :: MSUALG_5:13 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"   ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "C")) "being"   ($#v2_msualg_4 :::"MSEquivalence-like"::: )    ($#m1_msualg_4 :::"ManySortedRelation":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "C"))  ($#r8_pboole :::"="::: )  (Set (Set (Var "C1"))  ($#k4_msualg_5 :::""\/""::: )  (Set (Var "C2"))))) "holds"  (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "b1")) "being"   ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "a1")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "a1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "a2")))) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "a1"))))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "a1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")) ")" ) "," (Set  "(" (Set (Var "a2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Set (Var "C"))  ($#k2_msualg_4 :::"."::: )  (Set  "(" (Set  "("  ($#k1_msualg_1 :::"the_arity_of"::: )  (Set (Var "o")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")) ")" )))  ")" ) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set  "("  ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," (Set (Var "A")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "a1"))  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x1")) ($#k9_finseq_1 :::"*>"::: ) ) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set (Var "b1")) ")" ) ")" ) "," (Set  "(" (Set  "("  ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," (Set (Var "A")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "a2"))  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x1")) ($#k9_finseq_1 :::"*>"::: ) ) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set (Var "b1")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Set (Var "C"))  ($#k2_msualg_4 :::"."::: )  (Set  "("  ($#k2_msualg_1 :::"the_result_sort_of"::: )  (Set (Var "o")) ")" ))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Set (Var "C"))  ($#k2_msualg_4 :::"."::: )  (Set  "(" (Set  "("  ($#k1_msualg_1 :::"the_arity_of"::: )  (Set (Var "o")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))) "holds"  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_msualg_1 :::"Args"::: )   "(" (Set (Var "o")) "," (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a1"))  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x1")) ($#k9_finseq_1 :::"*>"::: ) ) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set (Var "b1"))))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set  "("  ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ) "," (Set  "(" (Set  "("  ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," (Set (Var "A")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "a2"))  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "y1")) ($#k9_finseq_1 :::"*>"::: ) ) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set (Var "b1")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Set (Var "C"))  ($#k2_msualg_4 :::"."::: )  (Set  "("  ($#k2_msualg_1 :::"the_result_sort_of"::: )  (Set (Var "o")) ")" )))))))))))) ; 
 
theorem :: MSUALG_5:14 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"   ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "C")) "being"   ($#v2_msualg_4 :::"MSEquivalence-like"::: )    ($#m1_msualg_4 :::"ManySortedRelation":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "C"))  ($#r8_pboole :::"="::: )  (Set (Set (Var "C1"))  ($#k4_msualg_5 :::""\/""::: )  (Set (Var "C2"))))) "holds"  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_msualg_1 :::"Args"::: )   "(" (Set (Var "o")) "," (Set (Var "A")) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "x"))))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "x"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ) "," (Set  "(" (Set (Var "y"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Set (Var "C"))  ($#k2_msualg_4 :::"."::: )  (Set  "(" (Set  "("  ($#k1_msualg_1 :::"the_arity_of"::: )  (Set (Var "o")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" )))  ")" )) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set  "("  ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ) "," (Set  "(" (Set  "("  ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Set (Var "C"))  ($#k2_msualg_4 :::"."::: )  (Set  "("  ($#k2_msualg_1 :::"the_result_sort_of"::: )  (Set (Var "o")) ")" ))))))))) ; 
 
theorem :: MSUALG_5:15 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"   ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set (Var "C1"))  ($#k4_msualg_5 :::""\/""::: )  (Set (Var "C2"))) "is"   ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A")))))) ; 
 
theorem :: MSUALG_5:16 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"   ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set (Var "C1"))  ($#k3_pboole :::"/\"::: )  (Set (Var "C2"))) "is"   ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A")))))) ; 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "A" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); func  :::"CongrLatt"::: "A" ->   ($#v3_lattices :::"strict"::: )     ($#m2_nat_lat :::"SubLattice"::: )   "of" (Set   ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "A")) means :: MSUALG_5:def 6 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)) "iff" (Bool (Set (Var "x")) "is"   ($#m1_msualg_4 :::"MSCongruence":::) "of" "A")  ")" )); end; 






:: deftheorem    defines :::"CongrLatt"::: MSUALG_5:def 6 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "b3")) "being"   ($#v3_lattices :::"strict"::: )     ($#m2_nat_lat :::"SubLattice"::: )   "of" (Set   ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A")))) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_msualg_5 :::"CongrLatt"::: )  (Set (Var "A")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))) "iff" (Bool (Set (Var "x")) "is"   ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A")))  ")" ))  ")" )))); 
 
theorem :: MSUALG_5:17 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "holds"  (Bool (Set   ($#k2_msualg_3 :::"id"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A")))) "is"   ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A"))))) ; 
 
theorem :: MSUALG_5:18 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "holds"  (Bool (Set  ($#k6_pboole :::"[|"::: ) (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) ($#k6_pboole :::"|]"::: ) ) "is"   ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A"))))) ; 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "A" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); 
cluster (Set   ($#k6_msualg_5 :::"CongrLatt"::: )  "A") ->   ($#v3_lattices :::"strict"::: )     ($#v15_lattices :::"bounded"::: )   ; 
end; 
theorem :: MSUALG_5:19 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "holds"  (Bool (Set   ($#k5_lattices :::"Bottom"::: )  (Set  "("  ($#k6_msualg_5 :::"CongrLatt"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_msualg_3 :::"id"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))))))) ; 
 
theorem :: MSUALG_5:20 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "holds"  (Bool (Set   ($#k6_lattices :::"Top"::: )  (Set  "("  ($#k6_msualg_5 :::"CongrLatt"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k6_pboole :::"[|"::: ) (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) ($#k6_pboole :::"|]"::: ) )))) ; 
 
theorem :: MSUALG_5:21 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k2_msualg_5 :::"EqRelLatt"::: )  (Set (Var "X")) ")" ))) "iff" (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")))  ")" )) ;