:: UNIALG_3 semantic presentation begin definitionlet "U0" be ($#l1_unialg_1 :::"Universal_Algebra":::); mode :::"SubAlgebra-Family"::: "of" "U0" -> ($#m1_hidden :::"set"::: ) means :: UNIALG_3:def 1 (Bool "for" (Set (Var "U1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "U1")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Var "U1")) "is" ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" "U0")); end; :: deftheorem defines :::"SubAlgebra-Family"::: UNIALG_3:def 1 : (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")) "is" ($#m1_unialg_3 :::"SubAlgebra-Family"::: ) "of" (Set (Var "U0"))) "iff" (Bool "for" (Set (Var "U1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "U1")) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) "holds" (Bool (Set (Var "U1")) "is" ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "U0")))) ")" ))); registrationlet "U0" be ($#l1_unialg_1 :::"Universal_Algebra":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_unialg_3 :::"SubAlgebra-Family"::: ) "of" "U0"; end; definitionlet "U0" be ($#l1_unialg_1 :::"Universal_Algebra":::); :: original: :::"Sub"::: redefine func :::"Sub"::: "U0" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_unialg_3 :::"SubAlgebra-Family"::: ) "of" "U0"; let "U00" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_unialg_3 :::"SubAlgebra-Family"::: ) "of" (Set (Const "U0")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "U00" -> ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" "U0"; end; definitionlet "U0" be ($#l1_unialg_1 :::"Universal_Algebra":::); let "u" be ($#m2_unialg_3 :::"Element"::: ) "of" (Set ($#k1_unialg_3 :::"Sub"::: ) (Set (Const "U0"))); func :::"carr"::: "u" -> ($#m1_subset_1 :::"Subset":::) "of" "U0" means :: UNIALG_3:def 2 (Bool "ex" (Set (Var "U1")) "being" ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" "U0" "st" (Bool "(" (Bool "u" ($#r1_hidden :::"="::: ) (Set (Var "U1"))) & (Bool it ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U1")))) ")" )); end; :: deftheorem defines :::"carr"::: UNIALG_3:def 2 : (Bool "for" (Set (Var "U0")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "u")) "being" ($#m2_unialg_3 :::"Element"::: ) "of" (Set ($#k1_unialg_3 :::"Sub"::: ) (Set (Var "U0"))) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_unialg_3 :::"carr"::: ) (Set (Var "u")))) "iff" (Bool "ex" (Set (Var "U1")) "being" ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "U0")) "st" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "U1"))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U1")))) ")" )) ")" )))); definitionlet "U0" be ($#l1_unialg_1 :::"Universal_Algebra":::); func :::"Carr"::: "U0" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_unialg_3 :::"Sub"::: ) "U0" ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "U0") ")" ) means :: UNIALG_3:def 3 (Bool "for" (Set (Var "u")) "being" ($#m2_unialg_3 :::"Element"::: ) "of" (Set ($#k1_unialg_3 :::"Sub"::: ) "U0") "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set ($#k2_unialg_3 :::"carr"::: ) (Set (Var "u"))))); end; :: deftheorem defines :::"Carr"::: UNIALG_3:def 3 : (Bool "for" (Set (Var "U0")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_unialg_3 :::"Sub"::: ) (Set (Var "U0")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U0"))) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_unialg_3 :::"Carr"::: ) (Set (Var "U0")))) "iff" (Bool "for" (Set (Var "u")) "being" ($#m2_unialg_3 :::"Element"::: ) "of" (Set ($#k1_unialg_3 :::"Sub"::: ) (Set (Var "U0"))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set ($#k2_unialg_3 :::"carr"::: ) (Set (Var "u"))))) ")" ))); theorem :: UNIALG_3:1 (Bool "for" (Set (Var "U0")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "u")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set ($#k1_unialg_3 :::"Sub"::: ) (Set (Var "U0")))) "iff" (Bool "ex" (Set (Var "U1")) "being" ($#v1_unialg_1 :::"strict"::: ) ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "U0")) "st" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "U1")))) ")" ))) ; theorem :: UNIALG_3:2 (Bool "for" (Set (Var "U0")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "H")) "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 ($#k19_margrel1 :::"arity"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r2_unialg_2 :::"is_closed_on"::: ) (Set (Var "o"))) "iff" (Bool (Set (Set (Var "o")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "H"))) ")" )))) ; theorem :: UNIALG_3:3 (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 "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U0")))))) ; theorem :: UNIALG_3:4 (Bool "for" (Set (Var "U0")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "H")) "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 "H")) ($#r2_unialg_2 :::"is_closed_on"::: ) (Set (Var "o"))) & (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "o")) ($#k2_unialg_2 :::"/."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Var "o")))))) ; theorem :: UNIALG_3:5 (Bool "for" (Set (Var "U0")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) "holds" (Bool (Set ($#k6_unialg_2 :::"Constants"::: ) (Set (Var "U0"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "o")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) where o "is" ($#m5_margrel1 :::"operation":::) "of" (Set (Var "U0")) : (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "}" )) ; theorem :: UNIALG_3:6 (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"))) ($#r1_hidden :::"="::: ) (Set ($#k6_unialg_2 :::"Constants"::: ) (Set (Var "U1")))))) ; registrationlet "U0" be ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::); cluster -> ($#v2_unialg_2 :::"with_const_op"::: ) for ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" "U0"; end; theorem :: UNIALG_3:7 (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 ($#k6_unialg_2 :::"Constants"::: ) (Set (Var "U1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_unialg_2 :::"Constants"::: ) (Set (Var "U2")))))) ; definitionlet "U0" be ($#l1_unialg_1 :::"Universal_Algebra":::); redefine func :::"Carr"::: "U0" means :: UNIALG_3:def 4 (Bool "for" (Set (Var "u")) "being" ($#m2_unialg_3 :::"Element"::: ) "of" (Set ($#k1_unialg_3 :::"Sub"::: ) "U0") (Bool "for" (Set (Var "U1")) "being" ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" "U0" "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "U1")))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U1")))))); end; :: deftheorem defines :::"Carr"::: UNIALG_3:def 4 : (Bool "for" (Set (Var "U0")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_unialg_3 :::"Sub"::: ) (Set (Var "U0")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U0"))) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_unialg_3 :::"Carr"::: ) (Set (Var "U0")))) "iff" (Bool "for" (Set (Var "u")) "being" ($#m2_unialg_3 :::"Element"::: ) "of" (Set ($#k1_unialg_3 :::"Sub"::: ) (Set (Var "U0"))) (Bool "for" (Set (Var "U1")) "being" ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "U0")) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "U1")))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U1")))))) ")" ))); theorem :: UNIALG_3:8 (Bool "for" (Set (Var "U0")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "H")) "being" ($#v1_unialg_1 :::"strict"::: ) ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "U0")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "U0")) "holds" (Bool "(" (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k3_unialg_3 :::"Carr"::: ) (Set (Var "U0")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "H")))) "iff" (Bool (Set (Var "u")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))) ")" )))) ; theorem :: UNIALG_3:9 (Bool "for" (Set (Var "U0")) "being" ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "H")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_unialg_3 :::"Sub"::: ) (Set (Var "U0")) ")" ) "holds" (Bool (Bool "not" (Set (Set "(" ($#k3_unialg_3 :::"Carr"::: ) (Set (Var "U0")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "H"))) "is" ($#v1_xboole_0 :::"empty"::: ) )))) ; theorem :: UNIALG_3:10 (Bool "for" (Set (Var "U0")) "being" ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "U1")) "being" ($#v1_unialg_1 :::"strict"::: ) ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "U0")) "holds" (Bool (Set ($#k6_unialg_2 :::"Constants"::: ) (Set (Var "U0"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k3_unialg_3 :::"Carr"::: ) (Set (Var "U0")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "U1")))))) ; theorem :: UNIALG_3:11 (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")) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_unialg_2 :::"Constants"::: ) (Set (Var "U0"))))) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U1"))))))) ; theorem :: UNIALG_3:12 (Bool "for" (Set (Var "U0")) "being" ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "H")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_unialg_3 :::"Sub"::: ) (Set (Var "U0")) ")" ) "holds" (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set "(" (Set "(" ($#k3_unialg_3 :::"Carr"::: ) (Set (Var "U0")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "H")) ")" )) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0"))))) ; theorem :: UNIALG_3:13 (Bool "for" (Set (Var "U0")) "being" ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k12_unialg_2 :::"UnSubAlLattice"::: ) (Set (Var "U0")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_unialg_3 :::"Sub"::: ) (Set (Var "U0"))))) ; theorem :: UNIALG_3:14 (Bool "for" (Set (Var "U0")) "being" ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "H")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_unialg_3 :::"Sub"::: ) (Set (Var "U0")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0")) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set "(" (Set "(" ($#k3_unialg_3 :::"Carr"::: ) (Set (Var "U0")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "H")) ")" )))) "holds" (Bool (Set (Var "S")) "is" ($#v1_unialg_2 :::"opers_closed"::: ) )))) ; definitionlet "U0" be ($#v1_unialg_1 :::"strict"::: ) ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::); let "H" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_unialg_3 :::"Sub"::: ) (Set (Const "U0")) ")" ); func :::"meet"::: "H" -> ($#v1_unialg_1 :::"strict"::: ) ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" "U0" means :: UNIALG_3:def 5 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set "(" (Set "(" ($#k3_unialg_3 :::"Carr"::: ) "U0" ")" ) ($#k7_relset_1 :::".:"::: ) "H" ")" ))); end; :: deftheorem defines :::"meet"::: UNIALG_3:def 5 : (Bool "for" (Set (Var "U0")) "being" ($#v1_unialg_1 :::"strict"::: ) ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "H")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_unialg_3 :::"Sub"::: ) (Set (Var "U0")) ")" ) (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 ($#k4_unialg_3 :::"meet"::: ) (Set (Var "H")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set "(" (Set "(" ($#k3_unialg_3 :::"Carr"::: ) (Set (Var "U0")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "H")) ")" ))) ")" )))); theorem :: UNIALG_3:15 (Bool "for" (Set (Var "U0")) "being" ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "l1")) "," (Set (Var "l2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_unialg_2 :::"UnSubAlLattice"::: ) (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 "l1")) ($#r1_hidden :::"="::: ) (Set (Var "U1"))) & (Bool (Set (Var "l2")) ($#r1_hidden :::"="::: ) (Set (Var "U2")))) "holds" (Bool "(" (Bool (Set (Var "l1")) ($#r3_lattices :::"[="::: ) (Set (Var "l2"))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U2")))) ")" )))) ; theorem :: UNIALG_3:16 (Bool "for" (Set (Var "U0")) "being" ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "l1")) "," (Set (Var "l2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_unialg_2 :::"UnSubAlLattice"::: ) (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 "l1")) ($#r1_hidden :::"="::: ) (Set (Var "U1"))) & (Bool (Set (Var "l2")) ($#r1_hidden :::"="::: ) (Set (Var "U2")))) "holds" (Bool "(" (Bool (Set (Var "l1")) ($#r3_lattices :::"[="::: ) (Set (Var "l2"))) "iff" (Bool (Set (Var "U1")) "is" ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "U2"))) ")" )))) ; theorem :: UNIALG_3:17 (Bool "for" (Set (Var "U0")) "being" ($#v1_unialg_1 :::"strict"::: ) ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::) "holds" (Bool (Set ($#k12_unialg_2 :::"UnSubAlLattice"::: ) (Set (Var "U0"))) "is" ($#v15_lattices :::"bounded"::: ) )) ; registrationlet "U0" be ($#v1_unialg_1 :::"strict"::: ) ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::); cluster (Set ($#k12_unialg_2 :::"UnSubAlLattice"::: ) "U0") -> ($#v15_lattices :::"bounded"::: ) ; end; theorem :: UNIALG_3:18 (Bool "for" (Set (Var "U0")) "being" ($#v1_unialg_1 :::"strict"::: ) ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "U1")) "being" ($#v1_unialg_1 :::"strict"::: ) ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "U0")) "holds" (Bool (Set (Set "(" ($#k7_unialg_2 :::"GenUnivAlg"::: ) (Set "(" ($#k6_unialg_2 :::"Constants"::: ) (Set (Var "U0")) ")" ) ")" ) ($#k5_unialg_2 :::"/\"::: ) (Set (Var "U1"))) ($#r1_hidden :::"="::: ) (Set ($#k7_unialg_2 :::"GenUnivAlg"::: ) (Set "(" ($#k6_unialg_2 :::"Constants"::: ) (Set (Var "U0")) ")" ))))) ; theorem :: UNIALG_3:19 (Bool "for" (Set (Var "U0")) "being" ($#v1_unialg_1 :::"strict"::: ) ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::) "holds" (Bool (Set ($#k5_lattices :::"Bottom"::: ) (Set "(" ($#k12_unialg_2 :::"UnSubAlLattice"::: ) (Set (Var "U0")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_unialg_2 :::"GenUnivAlg"::: ) (Set "(" ($#k6_unialg_2 :::"Constants"::: ) (Set (Var "U0")) ")" )))) ; theorem :: UNIALG_3:20 (Bool "for" (Set (Var "U0")) "being" ($#v1_unialg_1 :::"strict"::: ) ($#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")) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0")) "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U0"))))) "holds" (Bool (Set (Set "(" ($#k7_unialg_2 :::"GenUnivAlg"::: ) (Set (Var "H")) ")" ) ($#k8_unialg_2 :::""\/""::: ) (Set (Var "U1"))) ($#r1_hidden :::"="::: ) (Set ($#k7_unialg_2 :::"GenUnivAlg"::: ) (Set (Var "H"))))))) ; theorem :: UNIALG_3:21 (Bool "for" (Set (Var "U0")) "being" ($#v1_unialg_1 :::"strict"::: ) ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0")) "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U0"))))) "holds" (Bool (Set ($#k6_lattices :::"Top"::: ) (Set "(" ($#k12_unialg_2 :::"UnSubAlLattice"::: ) (Set (Var "U0")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_unialg_2 :::"GenUnivAlg"::: ) (Set (Var "H")))))) ; theorem :: UNIALG_3:22 (Bool "for" (Set (Var "U0")) "being" ($#v1_unialg_1 :::"strict"::: ) ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::) "holds" (Bool (Set ($#k6_lattices :::"Top"::: ) (Set "(" ($#k12_unialg_2 :::"UnSubAlLattice"::: ) (Set (Var "U0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "U0")))) ; theorem :: UNIALG_3:23 (Bool "for" (Set (Var "U0")) "being" ($#v1_unialg_1 :::"strict"::: ) ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::) "holds" (Bool (Set ($#k12_unialg_2 :::"UnSubAlLattice"::: ) (Set (Var "U0"))) "is" ($#v4_lattice3 :::"complete"::: ) )) ; definitionlet "U01", "U02" be ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::); let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "U01"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "U02"))); func :::"FuncLatt"::: "F" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k12_unialg_2 :::"UnSubAlLattice"::: ) "U01" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k12_unialg_2 :::"UnSubAlLattice"::: ) "U02" ")" )) means :: UNIALG_3:def 6 (Bool "for" (Set (Var "U1")) "being" ($#v1_unialg_1 :::"strict"::: ) ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" "U01" (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Subset":::) "of" "U02" "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set "F" ($#k7_relset_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U1")))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "U1"))) ($#r1_hidden :::"="::: ) (Set ($#k7_unialg_2 :::"GenUnivAlg"::: ) (Set (Var "H")))))); end; :: deftheorem defines :::"FuncLatt"::: UNIALG_3:def 6 : (Bool "for" (Set (Var "U01")) "," (Set (Var "U02")) "being" ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U01"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U02"))) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k12_unialg_2 :::"UnSubAlLattice"::: ) (Set (Var "U01")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k12_unialg_2 :::"UnSubAlLattice"::: ) (Set (Var "U02")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_unialg_3 :::"FuncLatt"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "U1")) "being" ($#v1_unialg_1 :::"strict"::: ) ($#m1_unialg_2 :::"SubAlgebra"::: ) "of" (Set (Var "U01")) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U02")) "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_relset_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U1")))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "U1"))) ($#r1_hidden :::"="::: ) (Set ($#k7_unialg_2 :::"GenUnivAlg"::: ) (Set (Var "H")))))) ")" )))); theorem :: UNIALG_3:24 (Bool "for" (Set (Var "U0")) "being" ($#v1_unialg_1 :::"strict"::: ) ($#v2_unialg_2 :::"with_const_op"::: ) ($#l1_unialg_1 :::"Universal_Algebra":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U0"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U0"))) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "U0")))))) "holds" (Bool (Set ($#k5_unialg_3 :::"FuncLatt"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k12_unialg_2 :::"UnSubAlLattice"::: ) (Set (Var "U0")) ")" )))))) ;