:: MSUALG_8  semantic presentation begin  


























theorem :: MSUALG_8:1 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"FinSequence":::) "holds"   (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")))) "iff" (Bool  "("  (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "p")))) & (Bool (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "p"))))  ")" )  ")" ))) ; 
 scheme  :: MSUALG_8:sch 1 NonUniqSeqEx{ F1() ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ), P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "p")) "being"   ($#m1_hidden :::"FinSequence":::) "st"  (Bool  "("  (Bool (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set F1 "("  ")" ))) & (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   ($#k2_finseq_1 :::"Seg"::: )  (Set F1 "("  ")" )))) "holds"  (Bool P1[(Set (Var "k")) "," (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))])  ")" )  ")" ))
 provided
(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   ($#k2_finseq_1 :::"Seg"::: )  (Set F1 "("  ")" )))) "holds"  (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool P1[(Set (Var "k")) "," (Set (Var "x"))])))
 proof 


end; 
theorem :: MSUALG_8:2 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k2_msualg_5 :::"EqRelLatt"::: )  (Set (Var "Y")) ")" )  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "A"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "B")))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r3_lattices :::"[="::: )  (Set (Var "b"))) "iff" (Bool (Set (Var "A"))  ($#r1_relset_1 :::"c="::: )  (Set (Var "B")))  ")" )))) ; 
 registrationlet "Y" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k2_msualg_5 :::"EqRelLatt"::: )  "Y") ->   ($#v15_lattices :::"bounded"::: )   ; 
end; 
theorem :: MSUALG_8:3 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_lattices :::"Bottom"::: )  (Set  "("  ($#k2_msualg_5 :::"EqRelLatt"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set (Var "Y"))))) ; 
 
theorem :: MSUALG_8:4 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k6_lattices :::"Top"::: )  (Set  "("  ($#k2_msualg_5 :::"EqRelLatt"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_eqrel_1 :::"nabla"::: )  (Set (Var "Y"))))) ; 
 
theorem :: MSUALG_8:5 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k2_msualg_5 :::"EqRelLatt"::: )  (Set (Var "Y"))) "is"   ($#v4_lattice3 :::"complete"::: )  )) ; 
 registrationlet "Y" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k2_msualg_5 :::"EqRelLatt"::: )  "Y") ->   ($#v4_lattice3 :::"complete"::: )   ; 
end; 
theorem :: MSUALG_8:6 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_msualg_5 :::"EqRelLatt"::: )  (Set (Var "Y")) ")" ) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X"))) "is"   ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "Y"))))) ; 
 
theorem :: MSUALG_8:7 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_msualg_5 :::"EqRelLatt"::: )  (Set (Var "Y")) ")" ) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k15_lattice3 :::""\/""::: )  (Set (Var "X")))))) ; 
 
theorem :: MSUALG_8:8 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_msualg_5 :::"EqRelLatt"::: )  (Set (Var "Y")) ")" )  (Bool  "for" (Set (Var "R")) "being"   ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "R"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X"))))) "holds"  (Bool (Set   ($#k15_lattice3 :::""\/""::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_msualg_5 :::"EqCl"::: )  (Set (Var "R"))))))) ; 
 
theorem :: MSUALG_8:9 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_msualg_5 :::"EqRelLatt"::: )  (Set (Var "Y")) ")" )  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "R"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "R"))  ($#k2_relat_1 :::"~"::: )  ))))) ; 
 
theorem :: MSUALG_8:10 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_msualg_5 :::"EqRelLatt"::: )  (Set (Var "Y")) ")" )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "holds"  (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k15_lattice3 :::""\/""::: )  (Set (Var "X")))) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"FinSequence":::) "st"  (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" ) "," (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X"))))  ")" )  ")" ))  ")" ))) ; 
 begin  
theorem :: MSUALG_8:11 (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 "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k6_msualg_5 :::"CongrLatt"::: )  (Set (Var "A")) ")" ) "holds"  (Bool (Set   ($#k16_lattice3 :::""/\""::: )   "(" (Set (Var "B")) "," (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) ")" ) ")" ) "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")); let "E" be   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Const "A"))) ")" ); func  :::"CongrCl"::: "E" ->   ($#m1_msualg_4 :::"MSCongruence":::) "of" "A" equals :: MSUALG_8:def 1 (Set   ($#k16_lattice3 :::""/\""::: )   "("  "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "A") ")" ) : (Bool  "("  (Bool (Set (Var "x")) "is"   ($#m1_msualg_4 :::"MSCongruence":::) "of" "A") & (Bool "E"  ($#r3_lattices :::"[="::: )  (Set (Var "x")))  ")" )  "}"   "," (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "A") ")" ) ")" ); end; 







:: deftheorem    defines :::"CongrCl"::: MSUALG_8:def 1 :  (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 "E")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) ")" ) "holds"  (Bool (Set   ($#k1_msualg_8 :::"CongrCl"::: )  (Set (Var "E")))  ($#r1_hidden :::"="::: )  (Set   ($#k16_lattice3 :::""/\""::: )   "("  "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) ")" ) : (Bool  "("  (Bool (Set (Var "x")) "is"   ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A"))) & (Bool (Set (Var "E"))  ($#r3_lattices :::"[="::: )  (Set (Var "x")))  ")" )  "}"   "," (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "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")); let "X" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Const "A"))) ")" ); func  :::"CongrCl"::: "X" ->   ($#m1_msualg_4 :::"MSCongruence":::) "of" "A" equals :: MSUALG_8:def 2 (Set   ($#k16_lattice3 :::""/\""::: )   "("  "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "A") ")" ) : (Bool  "("  (Bool (Set (Var "x")) "is"   ($#m1_msualg_4 :::"MSCongruence":::) "of" "A") & (Bool "X"  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "x")))  ")" )  "}"   "," (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "A") ")" ) ")" ); end; 







:: deftheorem    defines :::"CongrCl"::: MSUALG_8:def 2 :  (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 "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) ")" ) "holds"  (Bool (Set   ($#k2_msualg_8 :::"CongrCl"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k16_lattice3 :::""/\""::: )   "("  "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) ")" ) : (Bool  "("  (Bool (Set (Var "x")) "is"   ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A"))) & (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "x")))  ")" )  "}"   "," (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) ")" ) ")" ))))); 
 
theorem :: MSUALG_8: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 "C")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) ")" )  "st" (Bool (Bool (Set (Var "C")) "is"   ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A")))) "holds"  (Bool (Set   ($#k1_msualg_8 :::"CongrCl"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Var "C")))))) ; 
 
theorem :: MSUALG_8: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 "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) ")" ) "holds"  (Bool (Set   ($#k1_msualg_8 :::"CongrCl"::: )  (Set  "("  ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "X")) "," (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) ")" ) ")"  ")" ))  ($#r8_pboole :::"="::: )  (Set   ($#k2_msualg_8 :::"CongrCl"::: )  (Set (Var "X"))))))) ; 
 
theorem :: MSUALG_8: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 "B1")) "," (Set (Var "B2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k6_msualg_5 :::"CongrLatt"::: )  (Set (Var "A")) ")" )  (Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"   ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "C1"))  ($#r1_hidden :::"="::: )  (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "B1")) "," (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) ")" ) ")" )) & (Bool (Set (Var "C2"))  ($#r1_hidden :::"="::: )  (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "B2")) "," (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) ")" ) ")" ))) "holds"  (Bool (Set (Set (Var "C1"))  ($#k4_msualg_5 :::""\/""::: )  (Set (Var "C2")))  ($#r1_hidden :::"="::: )  (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set  "(" (Set (Var "B1"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B2")) ")" ) "," (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) ")" ) ")" )))))) ; 
 
theorem :: MSUALG_8: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 "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k6_msualg_5 :::"CongrLatt"::: )  (Set (Var "A")) ")" ) "holds"  (Bool (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "X")) "," (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k15_lattice3 :::""\/""::: )   "("  "{"  (Set  "("  ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "X0")) "," (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) ")" ) ")"  ")" ) where X0 "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) ")" ) : (Bool (Set (Var "X0")) "is"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")))  "}"   "," (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) ")" ) ")" ))))) ; 
 
theorem :: MSUALG_8:16 (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 "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I"))  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set  "(" (Set (Var "M"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" ) (Bool  "ex" (Set (Var "E")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M")) "st"  (Bool  "("  (Bool (Set (Set (Var "E"))  ($#k1_msualg_4 :::"."::: )  (Set (Var "i")))  ($#r2_relset_1 :::"="::: )  (Set (Var "e"))) & (Bool  "("   "for" (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Var "j"))  ($#r1_hidden :::"<>"::: )  (Set (Var "i")))) "holds"  (Bool (Set (Set (Var "E"))  ($#k1_msualg_4 :::"."::: )  (Set (Var "j")))  ($#r2_relset_1 :::"="::: )  (Set   ($#k1_eqrel_1 :::"nabla"::: )  (Set  "(" (Set (Var "M"))  ($#k1_funct_1 :::"."::: )  (Set (Var "j")) ")" )))  ")" )  ")" )))))) ; 
 notationlet "I" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "M" be   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "i" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "I")); let "X" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set (Const "M")) ")" ); synonym  :::"EqRelSet":::  "(" "X" "," "i" ")"  for  :::"pi":::  "(" "M" "," "I" ")" ; 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 "i" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "I")); let "X" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set (Const "M")) ")" ); :: original: :::"EqRelSet"::: redefine func  :::"EqRelSet":::  "(" "X" "," "i" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_msualg_5 :::"EqRelLatt"::: )  (Set  "(" "M"  ($#k1_funct_1 :::"."::: )  "i" ")" ) ")" ) means :: MSUALG_8:def 3 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "Eq")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" "M" "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "Eq"))  ($#k1_msualg_4 :::"."::: )  "i")) & (Bool (Set (Var "Eq"))  ($#r2_hidden :::"in"::: )  "X")  ")" ))  ")" )); end; 








:: deftheorem    defines :::"EqRelSet"::: MSUALG_8: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 "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set (Var "M")) ")" )  (Bool  "for" (Set (Var "b5")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_msualg_5 :::"EqRelLatt"::: )  (Set  "(" (Set (Var "M"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" ) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_msualg_8 :::"EqRelSet"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" )) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b5"))) "iff" (Bool  "ex" (Set (Var "Eq")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M")) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "Eq"))  ($#k1_msualg_4 :::"."::: )  (Set (Var "i")))) & (Bool (Set (Var "Eq"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" ))  ")" ))  ")" )))))); 
 
theorem :: MSUALG_8: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"))  (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) ")" )  (Bool  "for" (Set (Var "B")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A")))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set   ($#k15_lattice3 :::""\/""::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Set (Var "B"))  ($#k1_msualg_4 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set  "("  ($#k3_msualg_8 :::"EqRelSet"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")"  ")" ) "," (Set  "("  ($#k2_msualg_5 :::"EqRelLatt"::: )  (Set  "(" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A")))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" ) ")" ) ")" ))))))) ; 
 
theorem :: MSUALG_8: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"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k6_msualg_5 :::"CongrLatt"::: )  (Set (Var "A")) ")" ) "holds"  (Bool (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "X")) "," (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) ")" ) ")" ) "is"   ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A")))))) ; 
 
theorem :: MSUALG_8: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   ($#k6_msualg_5 :::"CongrLatt"::: )  (Set (Var "A"))) "is"   ($#v1_msualg_7 :::"/\-inheriting"::: )  ))) ; 
 
theorem :: MSUALG_8: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_msualg_5 :::"CongrLatt"::: )  (Set (Var "A"))) "is"   ($#v2_msualg_7 :::"\/-inheriting"::: )  ))) ; 
 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") ->   ($#v1_msualg_7 :::"/\-inheriting"::: )     ($#v2_msualg_7 :::"\/-inheriting"::: )   ; 
end;