:: UNIALG_2  semantic presentation begin  












definitionlet "U1" be   ($#l1_unialg_1 :::"Universal_Algebra":::); mode PFuncsDomHQN of "U1" is    ($#m4_margrel1 :::"PFuncsDomHQN"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "U1"); end; definitionlet "U1" be    ($#l1_unialg_1 :::"UAStr"::: )  ; mode PartFunc of "U1" is   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "U1")  ($#k3_finseq_2 :::"*"::: )  ")" ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "U1"); end; definitionlet "U1", "U2" be   ($#l1_unialg_1 :::"Universal_Algebra":::); pred "U1" "," "U2" :::"are_similar":::  means :: UNIALG_2:def 1 (Bool (Set   ($#k1_unialg_1 :::"signature"::: )  "U1")  ($#r1_hidden :::"="::: )  (Set   ($#k1_unialg_1 :::"signature"::: )  "U2")); symmetry  
(Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  "st" (Bool (Bool (Set   ($#k1_unialg_1 :::"signature"::: )  (Set (Var "U1")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_unialg_1 :::"signature"::: )  (Set (Var "U2"))))) "holds"  (Bool (Set   ($#k1_unialg_1 :::"signature"::: )  (Set (Var "U2")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_unialg_1 :::"signature"::: )  (Set (Var "U1")))))
 ; reflexivity  
(Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k1_unialg_1 :::"signature"::: )  (Set (Var "U1")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_unialg_1 :::"signature"::: )  (Set (Var "U1")))))
 ; end; 





:: deftheorem    defines :::"are_similar"::: UNIALG_2:def 1 :  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"   (Bool  "("  (Bool (Set (Var "U1")) "," (Set (Var "U2"))  ($#r1_unialg_2 :::"are_similar"::: )  ) "iff" (Bool (Set   ($#k1_unialg_1 :::"signature"::: )  (Set (Var "U1")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_unialg_1 :::"signature"::: )  (Set (Var "U2"))))  ")" )); 
 
theorem :: UNIALG_2:1 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  "st" (Bool (Bool (Set (Var "U1")) "," (Set (Var "U2"))  ($#r1_unialg_2 :::"are_similar"::: )  )) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U1"))))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U2")))))) ; 
 
theorem :: UNIALG_2:2 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "," (Set (Var "U3")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  "st" (Bool (Bool (Set (Var "U1")) "," (Set (Var "U2"))  ($#r1_unialg_2 :::"are_similar"::: )  ) & (Bool (Set (Var "U2")) "," (Set (Var "U3"))  ($#r1_unialg_2 :::"are_similar"::: )  )) "holds"  (Bool (Set (Var "U1")) "," (Set (Var "U3"))  ($#r1_unialg_2 :::"are_similar"::: )  )) ; 
 
theorem :: UNIALG_2:3 (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U0")))) "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_partfun1 :::"PFuncs"::: )   "(" (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U0")))  ($#k3_finseq_2 :::"*"::: )  ")" ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U0"))) ")"  ")" ))) ; 
 definitionlet "U0" be   ($#l1_unialg_1 :::"Universal_Algebra":::); func  :::"Operations"::: "U0" ->   ($#m4_margrel1 :::"PFuncsDomHQN":::) "of" "U0" equals :: UNIALG_2:def 2 (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "U0")); end; 





:: deftheorem    defines :::"Operations"::: UNIALG_2:def 2 :  (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k1_unialg_2 :::"Operations"::: )  (Set (Var "U0")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U0")))))); 
 definitionlet "U1" be   ($#l1_unialg_1 :::"Universal_Algebra":::); mode operation of "U1" is    ($#m5_margrel1 :::"Element"::: )   "of" (Set   ($#k1_unialg_2 :::"Operations"::: )  "U1"); end; 









definitionlet "U0" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "U0")); let "o" be   ($#m5_margrel1 :::"operation":::) "of" (Set (Const "U0")); pred "A" :::"is_closed_on"::: "o" means :: UNIALG_2:def 3 (Bool  "for" (Set (Var "s")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" "A"  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k19_margrel1 :::"arity"::: )  "o"))) "holds"  (Bool (Set "o"  ($#k1_funct_1 :::"."::: )  (Set (Var "s")))  ($#r2_hidden :::"in"::: )  "A")); end; 






:: deftheorem    defines :::"is_closed_on"::: UNIALG_2:def 3 :  (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0"))  (Bool  "for" (Set (Var "o")) "being"   ($#m5_margrel1 :::"operation":::) "of" (Set (Var "U0")) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r2_unialg_2 :::"is_closed_on"::: )  (Set (Var "o"))) "iff" (Bool  "for" (Set (Var "s")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k19_margrel1 :::"arity"::: )  (Set (Var "o"))))) "holds"  (Bool (Set (Set (Var "o"))  ($#k1_funct_1 :::"."::: )  (Set (Var "s")))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))))  ")" )))); 
 definitionlet "U0" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "U0")); attr "A" is  :::"opers_closed":::  means :: UNIALG_2:def 4 (Bool  "for" (Set (Var "o")) "being"   ($#m5_margrel1 :::"operation":::) "of" "U0" "holds"  (Bool "A"  ($#r2_unialg_2 :::"is_closed_on"::: )  (Set (Var "o")))); end; 





:: deftheorem    defines :::"opers_closed"::: UNIALG_2:def 4 :  (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0")) "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v1_unialg_2 :::"opers_closed"::: )  ) "iff" (Bool  "for" (Set (Var "o")) "being"   ($#m5_margrel1 :::"operation":::) "of" (Set (Var "U0")) "holds"  (Bool (Set (Var "A"))  ($#r2_unialg_2 :::"is_closed_on"::: )  (Set (Var "o"))))  ")" ))); 
 definitionlet "U0" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "U0")); let "o" be   ($#m5_margrel1 :::"operation":::) "of" (Set (Const "U0")); assume 
(Bool (Set (Const "A"))  ($#r2_unialg_2 :::"is_closed_on"::: )  (Set (Const "o")))
 ; func "o" :::"/."::: "A" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_margrel1 :::"homogeneous"::: )     ($#v3_margrel1 :::"quasi_total"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "(" "A"  ($#k3_finseq_2 :::"*"::: )  ")" ) "," "A" equals :: UNIALG_2:def 5 (Set "o"  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set  "("  ($#k19_margrel1 :::"arity"::: )  "o" ")" )  ($#k4_finseq_2 :::"-tuples_on"::: )  "A" ")" )); end; 








:: deftheorem    defines :::"/."::: UNIALG_2:def 5 :  (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0"))  (Bool  "for" (Set (Var "o")) "being"   ($#m5_margrel1 :::"operation":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_unialg_2 :::"is_closed_on"::: )  (Set (Var "o")))) "holds"  (Bool (Set (Set (Var "o"))  ($#k2_unialg_2 :::"/."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "o"))  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set  "("  ($#k19_margrel1 :::"arity"::: )  (Set (Var "o")) ")" )  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set (Var "A")) ")" )))))); 
 definitionlet "U0" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "U0")); func  :::"Opers":::  "(" "U0" "," "A" ")"  ->   ($#m2_finseq_1 :::"PFuncFinSequence":::) "of" "A" means :: UNIALG_2:def 6 (Bool  "("  (Bool (Set   ($#k4_finseq_1 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "U0"))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "o")) "being"   ($#m5_margrel1 :::"operation":::) "of" "U0"  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  it)) & (Bool (Set (Var "o"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "U0")  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "o"))  ($#k2_unialg_2 :::"/."::: )  "A")))  ")" )  ")" ); end; 






:: deftheorem    defines :::"Opers"::: UNIALG_2:def 6 :  (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m2_finseq_1 :::"PFuncFinSequence":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_unialg_2 :::"Opers"::: )   "(" (Set (Var "U0")) "," (Set (Var "A")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U0"))))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "o")) "being"   ($#m5_margrel1 :::"operation":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "b3")))) & (Bool (Set (Var "o"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U0")))  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "o"))  ($#k2_unialg_2 :::"/."::: )  (Set (Var "A")))))  ")" )  ")" )  ")" )))); 
 
theorem :: UNIALG_2:4 (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U0"))))) "holds"  (Bool  "("  (Bool (Set (Var "B")) "is"   ($#v1_unialg_2 :::"opers_closed"::: )  ) & (Bool  "("   "for" (Set (Var "o")) "being"   ($#m5_margrel1 :::"operation":::) "of" (Set (Var "U0")) "holds"  (Bool (Set (Set (Var "o"))  ($#k2_unialg_2 :::"/."::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Var "o")))  ")" )  ")" ))) ; 
 
theorem :: UNIALG_2:5 (Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U1"))  (Bool  "for" (Set (Var "o")) "being"   ($#m5_margrel1 :::"operation":::) "of" (Set (Var "U1"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_unialg_2 :::"is_closed_on"::: )  (Set (Var "o")))) "holds"  (Bool (Set   ($#k19_margrel1 :::"arity"::: )  (Set  "(" (Set (Var "o"))  ($#k2_unialg_2 :::"/."::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k19_margrel1 :::"arity"::: )  (Set (Var "o"))))))) ; 
 definitionlet "U0" be   ($#l1_unialg_1 :::"Universal_Algebra":::); mode  :::"SubAlgebra":::  "of" "U0" ->   ($#l1_unialg_1 :::"Universal_Algebra":::) means :: UNIALG_2:def 7 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it) "is"   ($#m1_subset_1 :::"Subset":::) "of" "U0") & (Bool  "("   "for" (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" "U0"  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it))) "holds"  (Bool  "("  (Bool (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k3_unialg_2 :::"Opers"::: )   "(" "U0" "," (Set (Var "B")) ")" )) & (Bool (Set (Var "B")) "is"   ($#v1_unialg_2 :::"opers_closed"::: )  )  ")" )  ")" )  ")" ); end; 





:: deftheorem    defines :::"SubAlgebra"::: UNIALG_2:def 7 :  (Bool  "for" (Set (Var "U0")) "," (Set (Var "b2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0"))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2"))) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0"))) & (Bool  "("   "for" (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2"))))) "holds"  (Bool  "("  (Bool (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_unialg_2 :::"Opers"::: )   "(" (Set (Var "U0")) "," (Set (Var "B")) ")" )) & (Bool (Set (Var "B")) "is"   ($#v1_unialg_2 :::"opers_closed"::: )  )  ")" )  ")" )  ")" )  ")" )); 
 registrationlet "U0" be   ($#l1_unialg_1 :::"Universal_Algebra":::); 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_unialg_1 :::"strict"::: )   bbbadV2_UNIALG_1()   ($#v3_unialg_1 :::"quasi_total"::: )     ($#v4_unialg_1 :::"non-empty"::: )    for    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" "U0"; 
end; 
theorem :: UNIALG_2:6 (Bool  "for" (Set (Var "U0")) "," (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "o0")) "being"   ($#m5_margrel1 :::"operation":::) "of" (Set (Var "U0"))  (Bool  "for" (Set (Var "o1")) "being"   ($#m5_margrel1 :::"operation":::) "of" (Set (Var "U1"))  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "U0")) "is"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U1"))) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U0"))))) & (Bool (Set (Var "o0"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U0")))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))) & (Bool (Set (Var "o1"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U1")))  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))))) "holds"  (Bool (Set   ($#k19_margrel1 :::"arity"::: )  (Set (Var "o0")))  ($#r1_hidden :::"="::: )  (Set   ($#k19_margrel1 :::"arity"::: )  (Set (Var "o1")))))))) ; 
 
theorem :: UNIALG_2:7 (Bool  "for" (Set (Var "U0")) "," (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  "st" (Bool (Bool (Set (Var "U0")) "is"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U1")))) "holds"  (Bool (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U0"))))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U1")))))) ; 
 
theorem :: UNIALG_2:8 (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set (Var "U0")) "is"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0")))) ; 
 
theorem :: UNIALG_2:9 (Bool  "for" (Set (Var "U0")) "," (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  "st" (Bool (Bool (Set (Var "U0")) "is"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U1"))) & (Bool (Set (Var "U1")) "is"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U2")))) "holds"  (Bool (Set (Var "U0")) "is"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U2")))) ; 
 
theorem :: UNIALG_2:10 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  "st" (Bool (Bool (Set (Var "U1")) "is"   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U2"))) & (Bool (Set (Var "U2")) "is"   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U1")))) "holds"  (Bool (Set (Var "U1"))  ($#r1_hidden :::"="::: )  (Set (Var "U2")))) ; 
 
theorem :: UNIALG_2:11 (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0"))  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U2"))))) "holds"  (Bool (Set (Var "U1")) "is"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U2"))))) ; 
 
theorem :: UNIALG_2:12 (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0"))  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U2"))))) "holds"  (Bool (Set (Var "U1"))  ($#r1_hidden :::"="::: )  (Set (Var "U2"))))) ; 
 
theorem :: UNIALG_2:13 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  "st" (Bool (Bool (Set (Var "U1")) "is"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U2")))) "holds"  (Bool (Set (Var "U1")) "," (Set (Var "U2"))  ($#r1_unialg_2 :::"are_similar"::: )  )) ; 
 
theorem :: UNIALG_2:14 (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0")) "holds"  (Bool (Set   ($#g1_unialg_1 :::"UAStr"::: )  "(#"  (Set (Var "A")) "," (Set  "("  ($#k3_unialg_2 :::"Opers"::: )   "(" (Set (Var "U0")) "," (Set (Var "A")) ")"  ")" ) "#)" ) "is"   ($#v1_unialg_1 :::"strict"::: )    ($#l1_unialg_1 :::"Universal_Algebra":::)))) ; 
 definitionlet "U0" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "U0")); assume 
(Bool (Set (Const "A")) "is"   ($#v1_unialg_2 :::"opers_closed"::: )  )
 ; func  :::"UniAlgSetClosed"::: "A" ->   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" "U0" equals :: UNIALG_2:def 8 (Set   ($#g1_unialg_1 :::"UAStr"::: )  "(#"  "A" "," (Set  "("  ($#k3_unialg_2 :::"Opers"::: )   "(" "U0" "," "A" ")"  ")" ) "#)" ); end; 







:: deftheorem    defines :::"UniAlgSetClosed"::: UNIALG_2:def 8 :  (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_unialg_2 :::"opers_closed"::: )  )) "holds"  (Bool (Set   ($#k4_unialg_2 :::"UniAlgSetClosed"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#g1_unialg_1 :::"UAStr"::: )  "(#"  (Set (Var "A")) "," (Set  "("  ($#k3_unialg_2 :::"Opers"::: )   "(" (Set (Var "U0")) "," (Set (Var "A")) ")"  ")" ) "#)" )))); 
 definitionlet "U0" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "U1", "U2" be    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Const "U0")); assume 
(Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "U1")))  ($#r2_subset_1 :::"meets"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "U2"))))
 ; func "U1" :::"/\"::: "U2" ->   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" "U0" means :: UNIALG_2:def 9 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "U1")  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "U2"))) & (Bool  "("   "for" (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" "U0"  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it))) "holds"  (Bool  "("  (Bool (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k3_unialg_2 :::"Opers"::: )   "(" "U0" "," (Set (Var "B")) ")" )) & (Bool (Set (Var "B")) "is"   ($#v1_unialg_2 :::"opers_closed"::: )  )  ")" )  ")" )  ")" ); end; 








:: deftheorem    defines :::"/\"::: UNIALG_2:def 9 :  (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0"))  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1")))  ($#r2_subset_1 :::"meets"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U2"))))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "U1"))  ($#k5_unialg_2 :::"/\"::: )  (Set (Var "U2")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U2"))))) & (Bool  "("   "for" (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b4"))))) "holds"  (Bool  "("  (Bool (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_unialg_2 :::"Opers"::: )   "(" (Set (Var "U0")) "," (Set (Var "B")) ")" )) & (Bool (Set (Var "B")) "is"   ($#v1_unialg_2 :::"opers_closed"::: )  )  ")" )  ")" )  ")" )  ")" )))); 
 definitionlet "U0" be   ($#l1_unialg_1 :::"Universal_Algebra":::); func  :::"Constants"::: "U0" ->   ($#m1_subset_1 :::"Subset":::) "of" "U0" equals :: UNIALG_2:def 10  "{"  (Set (Var "a")) where a "is"   ($#m1_subset_1 :::"Element":::) "of" "U0" : (Bool  "ex" (Set (Var "o")) "being"   ($#m5_margrel1 :::"operation":::) "of" "U0" "st"  (Bool  "("  (Bool (Set   ($#k19_margrel1 :::"arity"::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "o"))))  ")" ))  "}"  ; end; 





:: deftheorem    defines :::"Constants"::: UNIALG_2:def 10 :  (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k6_unialg_2 :::"Constants"::: )  (Set (Var "U0")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "a")) where a "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "U0")) : (Bool  "ex" (Set (Var "o")) "being"   ($#m5_margrel1 :::"operation":::) "of" (Set (Var "U0")) "st"  (Bool  "("  (Bool (Set   ($#k19_margrel1 :::"arity"::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "o"))))  ")" ))  "}"  )); 
 definitionlet "IT" be   ($#l1_unialg_1 :::"Universal_Algebra":::); attr "IT" is  :::"with_const_op":::  means :: UNIALG_2:def 11 (Bool  "ex" (Set (Var "o")) "being"   ($#m5_margrel1 :::"operation":::) "of" "IT" "st" (Bool (Set   ($#k19_margrel1 :::"arity"::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))); end; 




:: deftheorem    defines :::"with_const_op"::: UNIALG_2:def 11 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_unialg_2 :::"with_const_op"::: )  ) "iff" (Bool  "ex" (Set (Var "o")) "being"   ($#m5_margrel1 :::"operation":::) "of" (Set (Var "IT")) "st" (Bool (Set   ($#k19_margrel1 :::"arity"::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_unialg_1 :::"strict"::: )   bbbadV2_UNIALG_1()   ($#v3_unialg_1 :::"quasi_total"::: )     ($#v4_unialg_1 :::"non-empty"::: )     ($#v2_unialg_2 :::"with_const_op"::: )    for    ($#l1_unialg_1 :::"UAStr"::: )  ; 
end; registrationlet "U0" be   ($#v2_unialg_2 :::"with_const_op"::: )    ($#l1_unialg_1 :::"Universal_Algebra":::); 
cluster (Set   ($#k6_unialg_2 :::"Constants"::: )  "U0") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: UNIALG_2:15 (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "U1")) "being"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0")) "holds"  (Bool (Set   ($#k6_unialg_2 :::"Constants"::: )  (Set (Var "U0"))) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U1"))))) ; 
 
theorem :: UNIALG_2:16 (Bool  "for" (Set (Var "U0")) "being"   ($#v2_unialg_2 :::"with_const_op"::: )    ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "U1")) "being"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0")) "holds"  (Bool (Set   ($#k6_unialg_2 :::"Constants"::: )  (Set (Var "U0"))) "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U1"))))) ; 
 
theorem :: UNIALG_2:17 (Bool  "for" (Set (Var "U0")) "being"   ($#v2_unialg_2 :::"with_const_op"::: )    ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0"))  "holds" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1")))  ($#r2_subset_1 :::"meets"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U2")))))) ; 
 definitionlet "U0" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "U0")); assume 
(Bool  "("  (Bool (Set   ($#k6_unialg_2 :::"Constants"::: )  (Set (Const "U0")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set (Const "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )
 ; func  :::"GenUnivAlg"::: "A" ->   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" "U0" means :: UNIALG_2:def 12 (Bool  "("  (Bool "A"  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)) & (Bool  "("   "for" (Set (Var "U1")) "being"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" "U0"  "st" (Bool (Bool "A"  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1"))))) "holds"  (Bool it "is"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U1")))  ")" )  ")" ); end; 







:: deftheorem    defines :::"GenUnivAlg"::: UNIALG_2:def 12 :  (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool  "("  (Bool (Set   ($#k6_unialg_2 :::"Constants"::: )  (Set (Var "U0")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_unialg_2 :::"GenUnivAlg"::: )  (Set (Var "A")))) "iff" (Bool  "("  (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))) & (Bool  "("   "for" (Set (Var "U1")) "being"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1"))))) "holds"  (Bool (Set (Var "b3")) "is"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U1")))  ")" )  ")" )  ")" )))); 
 
theorem :: UNIALG_2:18 (Bool  "for" (Set (Var "U0")) "being"   ($#v1_unialg_1 :::"strict"::: )    ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k7_unialg_2 :::"GenUnivAlg"::: )  (Set  "("  ($#k2_subset_1 :::"[#]"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U0"))) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "U0")))) ; 
 
theorem :: UNIALG_2:19 (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "U1")) "being"   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0"))  (Bool  "for" (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1"))))) "holds"  (Bool (Set   ($#k7_unialg_2 :::"GenUnivAlg"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Var "U1")))))) ; 
 definitionlet "U0" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "U1", "U2" be    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Const "U0")); func "U1" :::""\/""::: "U2" ->   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" "U0" means :: UNIALG_2:def 13 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" "U0"  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "U1")  ($#k2_xboole_0 :::"\/"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "U2")))) "holds"  (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k7_unialg_2 :::"GenUnivAlg"::: )  (Set (Var "A"))))); end; 







:: deftheorem    defines :::""\/""::: UNIALG_2:def 13 :  (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0"))  (Bool  "for" (Set (Var "b4")) "being"   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "U1"))  ($#k8_unialg_2 :::""\/""::: )  (Set (Var "U2")))) "iff" (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1")))  ($#k2_xboole_0 :::"\/"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U2")))))) "holds"  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_unialg_2 :::"GenUnivAlg"::: )  (Set (Var "A")))))  ")" )))); 
 
theorem :: UNIALG_2:20 (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "U1")) "being"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set   ($#k6_unialg_2 :::"Constants"::: )  (Set (Var "U0")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" ) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1")))))) "holds"  (Bool (Set (Set  "("  ($#k7_unialg_2 :::"GenUnivAlg"::: )  (Set (Var "A")) ")" )  ($#k8_unialg_2 :::""\/""::: )  (Set (Var "U1")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_unialg_2 :::"GenUnivAlg"::: )  (Set (Var "B"))))))) ; 
 
theorem :: UNIALG_2:21 (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"    ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0")) "holds"  (Bool (Set (Set (Var "U1"))  ($#k8_unialg_2 :::""\/""::: )  (Set (Var "U2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "U2"))  ($#k8_unialg_2 :::""\/""::: )  (Set (Var "U1")))))) ; 
 
theorem :: UNIALG_2:22 (Bool  "for" (Set (Var "U0")) "being"   ($#v2_unialg_2 :::"with_const_op"::: )    ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0")) "holds"  (Bool (Set (Set (Var "U1"))  ($#k5_unialg_2 :::"/\"::: )  (Set  "(" (Set (Var "U1"))  ($#k8_unialg_2 :::""\/""::: )  (Set (Var "U2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "U1"))))) ; 
 
theorem :: UNIALG_2:23 (Bool  "for" (Set (Var "U0")) "being"   ($#v2_unialg_2 :::"with_const_op"::: )    ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0")) "holds"  (Bool (Set (Set  "(" (Set (Var "U1"))  ($#k5_unialg_2 :::"/\"::: )  (Set (Var "U2")) ")" )  ($#k8_unialg_2 :::""\/""::: )  (Set (Var "U2")))  ($#r1_hidden :::"="::: )  (Set (Var "U2"))))) ; 
 definitionlet "U0" be   ($#l1_unialg_1 :::"Universal_Algebra":::); func  :::"Sub"::: "U0" ->    ($#m1_hidden :::"set"::: )   means :: UNIALG_2:def 14 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "x")) "is"   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" "U0")  ")" )); end; 





:: deftheorem    defines :::"Sub"::: UNIALG_2:def 14 :  (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "b2")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_unialg_2 :::"Sub"::: )  (Set (Var "U0")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool (Set (Var "x")) "is"   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0")))  ")" ))  ")" ))); 
 registrationlet "U0" be   ($#l1_unialg_1 :::"Universal_Algebra":::); 
cluster (Set   ($#k9_unialg_2 :::"Sub"::: )  "U0") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; definitionlet "U0" be   ($#l1_unialg_1 :::"Universal_Algebra":::); func  :::"UniAlg_join"::: "U0" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k9_unialg_2 :::"Sub"::: )  "U0" ")" ) means :: UNIALG_2:def 15 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k9_unialg_2 :::"Sub"::: )  "U0")  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" "U0"  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "U1"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "U2")))) "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "U1"))  ($#k8_unialg_2 :::""\/""::: )  (Set (Var "U2")))))); end; 





:: deftheorem    defines :::"UniAlg_join"::: UNIALG_2:def 15 :  (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k9_unialg_2 :::"Sub"::: )  (Set (Var "U0")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_unialg_2 :::"UniAlg_join"::: )  (Set (Var "U0")))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k9_unialg_2 :::"Sub"::: )  (Set (Var "U0")))  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "U1"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "U2")))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "U1"))  ($#k8_unialg_2 :::""\/""::: )  (Set (Var "U2"))))))  ")" ))); 
 definitionlet "U0" be   ($#l1_unialg_1 :::"Universal_Algebra":::); func  :::"UniAlg_meet"::: "U0" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k9_unialg_2 :::"Sub"::: )  "U0" ")" ) means :: UNIALG_2:def 16 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k9_unialg_2 :::"Sub"::: )  "U0")  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" "U0"  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "U1"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "U2")))) "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "U1"))  ($#k5_unialg_2 :::"/\"::: )  (Set (Var "U2")))))); end; 





:: deftheorem    defines :::"UniAlg_meet"::: UNIALG_2:def 16 :  (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k9_unialg_2 :::"Sub"::: )  (Set (Var "U0")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_unialg_2 :::"UniAlg_meet"::: )  (Set (Var "U0")))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k9_unialg_2 :::"Sub"::: )  (Set (Var "U0")))  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "U1"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "U2")))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "U1"))  ($#k5_unialg_2 :::"/\"::: )  (Set (Var "U2"))))))  ")" ))); 
 
theorem :: UNIALG_2:24 (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k10_unialg_2 :::"UniAlg_join"::: )  (Set (Var "U0"))) "is"   ($#v1_binop_1 :::"commutative"::: )  )) ; 
 
theorem :: UNIALG_2:25 (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k10_unialg_2 :::"UniAlg_join"::: )  (Set (Var "U0"))) "is"   ($#v2_binop_1 :::"associative"::: )  )) ; 
 
theorem :: UNIALG_2:26 (Bool  "for" (Set (Var "U0")) "being"   ($#v2_unialg_2 :::"with_const_op"::: )    ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k11_unialg_2 :::"UniAlg_meet"::: )  (Set (Var "U0"))) "is"   ($#v1_binop_1 :::"commutative"::: )  )) ; 
 
theorem :: UNIALG_2:27 (Bool  "for" (Set (Var "U0")) "being"   ($#v2_unialg_2 :::"with_const_op"::: )    ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k11_unialg_2 :::"UniAlg_meet"::: )  (Set (Var "U0"))) "is"   ($#v2_binop_1 :::"associative"::: )  )) ; 
 definitionlet "U0" be   ($#v2_unialg_2 :::"with_const_op"::: )    ($#l1_unialg_1 :::"Universal_Algebra":::); func  :::"UnSubAlLattice"::: "U0" ->   ($#v3_lattices :::"strict"::: )    ($#l3_lattices :::"Lattice":::) equals :: UNIALG_2:def 17 (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "("  ($#k9_unialg_2 :::"Sub"::: )  "U0" ")" ) "," (Set  "("  ($#k10_unialg_2 :::"UniAlg_join"::: )  "U0" ")" ) "," (Set  "("  ($#k11_unialg_2 :::"UniAlg_meet"::: )  "U0" ")" ) "#)" ); end; 





:: deftheorem    defines :::"UnSubAlLattice"::: UNIALG_2:def 17 :  (Bool  "for" (Set (Var "U0")) "being"   ($#v2_unialg_2 :::"with_const_op"::: )    ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k12_unialg_2 :::"UnSubAlLattice"::: )  (Set (Var "U0")))  ($#r1_hidden :::"="::: )  (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "("  ($#k9_unialg_2 :::"Sub"::: )  (Set (Var "U0")) ")" ) "," (Set  "("  ($#k10_unialg_2 :::"UniAlg_join"::: )  (Set (Var "U0")) ")" ) "," (Set  "("  ($#k11_unialg_2 :::"UniAlg_meet"::: )  (Set (Var "U0")) ")" ) "#)" )));