:: ALTCAT_2 semantic presentation begin theorem :: ALTCAT_2:1 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k16_funct_3 :::"[:"::: ) (Set "(" (Set (Var "X1")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "a1")) ")" ) "," (Set "(" (Set (Var "X2")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "a2")) ")" ) ($#k16_funct_3 :::":]"::: ) ) ($#r1_funct_2 :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k4_tarski :::"]"::: ) )))) ; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_pboole :::"[[0]]"::: ) "I") -> ($#v1_funcop_1 :::"Function-yielding"::: ) ; end; theorem :: ALTCAT_2:2 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k2_funct_4 :::"~"::: ) (Set "(" (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k2_funct_4 :::"~"::: ) (Set (Var "f")) ")" )))) ; theorem :: ALTCAT_2:3 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k2_funct_4 :::"~"::: ) (Set "(" (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set ($#k15_funct_3 :::"[:"::: ) (Set (Var "g")) "," (Set (Var "h")) ($#k15_funct_3 :::":]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_funct_4 :::"~"::: ) (Set (Var "f")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set ($#k15_funct_3 :::"[:"::: ) (Set (Var "h")) "," (Set (Var "g")) ($#k15_funct_3 :::":]"::: ) )))) ; registrationlet "f" be ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k2_funct_4 :::"~"::: ) "f") -> ($#v1_funcop_1 :::"Function-yielding"::: ) ; end; theorem :: ALTCAT_2:4 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) ($#r1_pzfmisc1 :::"is_transformable_to"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "holds" (Bool (Set (Set (Var "G")) ($#k8_pboole :::"**"::: ) (Set (Var "F"))) "is" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "C"))))))) ; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "I")) "," (Set (Const "I")) ($#k2_zfmisc_1 :::":]"::: ) ); cluster (Set ($#k2_funct_4 :::"~"::: ) "A") -> (Set ($#k2_zfmisc_1 :::"[:"::: ) "I" "," "I" ($#k2_zfmisc_1 :::":]"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "I")) "," (Set (Const "I")) ($#k2_zfmisc_1 :::":]"::: ) ); cluster (Set ($#k2_funct_4 :::"~"::: ) "A") -> (Set ($#k2_zfmisc_1 :::"[:"::: ) "I" "," "I" ($#k2_zfmisc_1 :::":]"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for(Set ($#k2_zfmisc_1 :::"[:"::: ) "I" "," "I" ($#k2_zfmisc_1 :::":]"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); end; theorem :: ALTCAT_2:5 (Bool "for" (Set (Var "I1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "I2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I1")) "," (Set (Var "I2")) (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I2")) (Bool "for" (Set (Var "G")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "holds" (Bool (Set (Set (Var "G")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) "is" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Set (Var "B")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) "," (Set (Set (Var "C")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "I")) "," (Set (Const "I")) ($#k2_zfmisc_1 :::":]"::: ) ); let "F" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); :: original: :::"~"::: redefine func :::"~"::: "F" -> ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set ($#k2_funct_4 :::"~"::: ) "A") "," (Set ($#k2_funct_4 :::"~"::: ) "B"); end; theorem :: ALTCAT_2:6 (Bool "for" (Set (Var "I1")) "," (Set (Var "I2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "I1")) "," (Set (Var "I2")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I1")) (Bool "for" (Set (Var "o2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I2")) "holds" (Bool (Set (Set "(" ($#k2_funct_4 :::"~"::: ) (Set (Var "M")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "o2")) "," (Set (Var "o1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "o1")) "," (Set (Var "o2")) ")" )))))) ; registrationlet "I1" be ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Const "I1")); cluster (Set "g" ($#k8_pboole :::"**"::: ) "f") -> "I1" ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "I1" be ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Const "I1")); cluster (Set "g" ($#k8_pboole :::"**"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) ; end; begin definitionlet "f", "g" be ($#m1_hidden :::"Function":::); pred "f" :::"cc="::: "g" means :: ALTCAT_2:def 1 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) "f") ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "g")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set "g" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ); reflexivity (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" )) ; end; :: deftheorem defines :::"cc="::: ALTCAT_2:def 1 : (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_altcat_2 :::"cc="::: ) (Set (Var "g"))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" )); definitionlet "I", "J" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "J")); :: original: :::"cc="::: redefine pred "A" :::"cc="::: "B" means :: ALTCAT_2:def 2 (Bool "(" (Bool "I" ($#r1_tarski :::"c="::: ) "J") & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set "A" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set "B" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ); end; :: deftheorem defines :::"cc="::: ALTCAT_2:def 2 : (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_altcat_2 :::"cc="::: ) (Set (Var "B"))) "iff" (Bool "(" (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "J"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" )))); theorem :: ALTCAT_2:7 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) "st" (Bool (Bool (Set (Var "A")) ($#r2_altcat_2 :::"cc="::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) ($#r2_altcat_2 :::"cc="::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))))) ; theorem :: ALTCAT_2:8 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "," (Set (Var "K")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "A")) ($#r2_altcat_2 :::"cc="::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) ($#r2_altcat_2 :::"cc="::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "A")) ($#r2_altcat_2 :::"cc="::: ) (Set (Var "C"))))))) ; theorem :: ALTCAT_2:9 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_altcat_2 :::"cc="::: ) (Set (Var "B"))) "iff" (Bool (Set (Var "A")) ($#r2_pboole :::"c="::: ) (Set (Var "B"))) ")" ))) ; begin scheme :: ALTCAT_2:sch 1 OnSingletons{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set F2 "(" (Set (Var "o")) ")" ) ($#k4_tarski :::"]"::: ) ) where o "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "o"))]) "}" "is" ($#m1_hidden :::"Function":::)) proof end; scheme :: ALTCAT_2:sch 2 DomOnSingletons{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"Function":::), F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set F2 "(" ")" )) ($#r1_hidden :::"="::: ) "{" (Set (Var "o")) where o "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "o"))]) "}" ) provided (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set F3 "(" (Set (Var "o")) ")" ) ($#k4_tarski :::"]"::: ) ) where o "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "o"))]) "}" ) proof end; scheme :: ALTCAT_2:sch 3 ValOnSingletons{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"Function":::), F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F3 "(" ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set F3 "(" ")" ) ")" )) provided (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set F4 "(" (Set (Var "o")) ")" ) ($#k4_tarski :::"]"::: ) ) where o "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "o"))]) "}" ) and (Bool P1[(Set F3 "(" ")" )]) proof end; begin theorem :: ALTCAT_2:10 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "j")) "," (Set (Var "k")) ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k8_mcart_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set (Var "C"))))))) ; theorem :: ALTCAT_2:11 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set (Var "C"))) ($#k7_relat_1 :::".:"::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "j")) "," (Set (Var "k")) ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k8_mcart_1 :::":]"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "i")) "," (Set (Var "k")) ")" )))) ; definitionlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_cat_1 :::"CatStr"::: ) ; func :::"the_hom_sets_of"::: "C" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C") ($#k2_zfmisc_1 :::":]"::: ) ) means :: ALTCAT_2:def 3 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Object":::) "of" "C" "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))); end; :: deftheorem defines :::"the_hom_sets_of"::: ALTCAT_2:def 3 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_cat_1 :::"CatStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_altcat_2 :::"the_hom_sets_of"::: ) (Set (Var "C")))) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "b2")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))) ")" ))); theorem :: ALTCAT_2:12 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k2_altcat_2 :::"the_hom_sets_of"::: ) (Set (Var "C")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "i")) ")" )))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); func :::"the_comps_of"::: "C" -> ($#m2_pboole :::"BinComp":::) "of" (Set "(" ($#k2_altcat_2 :::"the_hom_sets_of"::: ) "C" ")" ) means :: ALTCAT_2:def 4 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Object":::) "of" "C" "holds" (Bool (Set it ($#k4_altcat_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" "C") ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set "(" ($#k2_altcat_2 :::"the_hom_sets_of"::: ) "C" ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "k")) ")" ")" ) "," (Set "(" (Set "(" ($#k2_altcat_2 :::"the_hom_sets_of"::: ) "C" ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )))); end; :: deftheorem defines :::"the_comps_of"::: ALTCAT_2:def 4 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b2")) "being" ($#m2_pboole :::"BinComp":::) "of" (Set "(" ($#k2_altcat_2 :::"the_hom_sets_of"::: ) (Set (Var "C")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_altcat_2 :::"the_comps_of"::: ) (Set (Var "C")))) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "b2")) ($#k4_altcat_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set (Var "C"))) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set "(" ($#k2_altcat_2 :::"the_hom_sets_of"::: ) (Set (Var "C")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "k")) ")" ")" ) "," (Set "(" (Set "(" ($#k2_altcat_2 :::"the_hom_sets_of"::: ) (Set (Var "C")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )))) ")" ))); theorem :: ALTCAT_2:13 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "j")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "i")) "," (Set (Var "j")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "j")) "," (Set (Var "k")) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_altcat_2 :::"the_comps_of"::: ) (Set (Var "C")) ")" ) ($#k4_altcat_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) ")" ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f")))))))) ; theorem :: ALTCAT_2:14 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set ($#k3_altcat_2 :::"the_comps_of"::: ) (Set (Var "C"))) "is" ($#v3_altcat_1 :::"associative"::: ) )) ; theorem :: ALTCAT_2:15 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool "(" (Bool (Set ($#k3_altcat_2 :::"the_comps_of"::: ) (Set (Var "C"))) "is" ($#v5_altcat_1 :::"with_left_units"::: ) ) & (Bool (Set ($#k3_altcat_2 :::"the_comps_of"::: ) (Set (Var "C"))) "is" ($#v4_altcat_1 :::"with_right_units"::: ) ) ")" )) ; begin definitionlet "C" be ($#l1_cat_1 :::"Category":::); func :::"Alter"::: "C" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_altcat_1 :::"strict"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) equals :: ALTCAT_2:def 5 (Set ($#g2_altcat_1 :::"AltCatStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C") "," (Set "(" ($#k2_altcat_2 :::"the_hom_sets_of"::: ) "C" ")" ) "," (Set "(" ($#k3_altcat_2 :::"the_comps_of"::: ) "C" ")" ) "#)" ); end; :: deftheorem defines :::"Alter"::: ALTCAT_2:def 5 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set ($#k4_altcat_2 :::"Alter"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#g2_altcat_1 :::"AltCatStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "," (Set "(" ($#k2_altcat_2 :::"the_hom_sets_of"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k3_altcat_2 :::"the_comps_of"::: ) (Set (Var "C")) ")" ) "#)" ))); theorem :: ALTCAT_2:16 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set ($#k4_altcat_2 :::"Alter"::: ) (Set (Var "C"))) "is" ($#v11_altcat_1 :::"associative"::: ) )) ; theorem :: ALTCAT_2:17 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set ($#k4_altcat_2 :::"Alter"::: ) (Set (Var "C"))) "is" ($#v12_altcat_1 :::"with_units"::: ) )) ; theorem :: ALTCAT_2:18 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set ($#k4_altcat_2 :::"Alter"::: ) (Set (Var "C"))) "is" ($#v2_altcat_1 :::"transitive"::: ) )) ; registrationlet "C" be ($#l1_cat_1 :::"Category":::); cluster (Set ($#k4_altcat_2 :::"Alter"::: ) "C") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v6_altcat_1 :::"strict"::: ) ($#v11_altcat_1 :::"associative"::: ) ($#v12_altcat_1 :::"with_units"::: ) ; end; begin registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_1 :::"strict"::: ) for ($#l1_altcat_1 :::"AltGraph"::: ) ; end; definitionlet "C" be ($#l1_altcat_1 :::"AltGraph"::: ) ; attr "C" is :::"reflexive"::: means :: ALTCAT_2:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C"))) "holds" (Bool (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" "C") ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))); end; :: deftheorem defines :::"reflexive"::: ALTCAT_2:def 6 : (Bool "for" (Set (Var "C")) "being" ($#l1_altcat_1 :::"AltGraph"::: ) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v1_altcat_2 :::"reflexive"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))))) "holds" (Bool (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "C"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" )); definitionlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; redefine attr "C" is :::"reflexive"::: means :: ALTCAT_2:def 7 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" "C" "holds" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "o")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))); end; :: deftheorem defines :::"reflexive"::: ALTCAT_2:def 7 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v1_altcat_2 :::"reflexive"::: ) ) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "o")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" )); definitionlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; redefine attr "C" is :::"associative"::: means :: ALTCAT_2:def 8 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "," (Set (Var "o4")) "being" ($#m1_subset_1 :::"object":::) "of" "C" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o3")) "," (Set (Var "o4")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o3")) "," (Set (Var "o4")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "h")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "g")) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k5_altcat_1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "f")) ")" ))))))); end; :: deftheorem defines :::"associative"::: ALTCAT_2:def 8 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v11_altcat_1 :::"associative"::: ) ) "iff" (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "," (Set (Var "o4")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o3")) "," (Set (Var "o4")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o3")) "," (Set (Var "o4")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "h")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "g")) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k5_altcat_1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "f")) ")" ))))))) ")" )); definitionlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; redefine attr "C" is :::"with_units"::: means :: ALTCAT_2:def 9 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" "C" "holds" (Bool "(" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "o")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o")) "," (Set (Var "o")) "st" (Bool "for" (Set (Var "o9")) "being" ($#m1_subset_1 :::"object":::) "of" "C" (Bool "for" (Set (Var "m9")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o9")) "," (Set (Var "o")) (Bool "for" (Set (Var "m99")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o")) "," (Set (Var "o9")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o9")) "," (Set (Var "o")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "i")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "m9"))) ($#r1_hidden :::"="::: ) (Set (Var "m9"))) ")" & "(" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "o9")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "m99")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "m99"))) ")" ")" ))))) ")" )); end; :: deftheorem defines :::"with_units"::: ALTCAT_2:def 9 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v12_altcat_1 :::"with_units"::: ) ) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "o")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o")) "," (Set (Var "o")) "st" (Bool "for" (Set (Var "o9")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "m9")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o9")) "," (Set (Var "o")) (Bool "for" (Set (Var "m99")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o")) "," (Set (Var "o9")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o9")) "," (Set (Var "o")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "i")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "m9"))) ($#r1_hidden :::"="::: ) (Set (Var "m9"))) ")" & "(" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "o9")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "m99")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "m99"))) ")" ")" ))))) ")" )) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) for ($#l2_altcat_1 :::"AltCatStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) for ($#l1_altcat_1 :::"AltGraph"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) for ($#l2_altcat_1 :::"AltCatStr"::: ) ; end; begin definitionfunc :::"the_empty_category"::: -> ($#v6_altcat_1 :::"strict"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) means :: ALTCAT_2:def 10 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) "is" ($#v1_xboole_0 :::"empty"::: ) ); end; :: deftheorem defines :::"the_empty_category"::: ALTCAT_2:def 10 : (Bool "for" (Set (Var "b1")) "being" ($#v6_altcat_1 :::"strict"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k5_altcat_2 :::"the_empty_category"::: ) )) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )); registration cluster (Set ($#k5_altcat_2 :::"the_empty_category"::: ) ) -> ($#v2_struct_0 :::"empty"::: ) ($#v6_altcat_1 :::"strict"::: ) ; end; registration cluster ($#v2_struct_0 :::"empty"::: ) ($#v6_altcat_1 :::"strict"::: ) for ($#l2_altcat_1 :::"AltCatStr"::: ) ; end; theorem :: ALTCAT_2:19 (Bool "for" (Set (Var "E")) "being" ($#v2_struct_0 :::"empty"::: ) ($#v6_altcat_1 :::"strict"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) "holds" (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k5_altcat_2 :::"the_empty_category"::: ) ))) ; begin definitionlet "C" be ($#l2_altcat_1 :::"AltCatStr"::: ) ; mode :::"SubCatStr"::: "of" "C" -> ($#l2_altcat_1 :::"AltCatStr"::: ) means :: ALTCAT_2:def 11 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C")) & (Bool (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" it) ($#r2_altcat_2 :::"cc="::: ) (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" "C")) & (Bool (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" it) ($#r2_altcat_2 :::"cc="::: ) (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" "C")) ")" ); end; :: deftheorem defines :::"SubCatStr"::: ALTCAT_2:def 11 : (Bool "for" (Set (Var "C")) "," (Set (Var "b2")) "being" ($#l2_altcat_1 :::"AltCatStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "C"))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C")))) & (Bool (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "b2"))) ($#r2_altcat_2 :::"cc="::: ) (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "C")))) & (Bool (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "b2"))) ($#r2_altcat_2 :::"cc="::: ) (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "C")))) ")" ) ")" )); theorem :: ALTCAT_2:20 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"AltCatStr"::: ) "holds" (Bool (Set (Var "C")) "is" ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "C")))) ; theorem :: ALTCAT_2:21 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) "being" ($#l2_altcat_1 :::"AltCatStr"::: ) "st" (Bool (Bool (Set (Var "C1")) "is" ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "C2"))) & (Bool (Set (Var "C2")) "is" ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "C3")))) "holds" (Bool (Set (Var "C1")) "is" ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "C3")))) ; theorem :: ALTCAT_2:22 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#l2_altcat_1 :::"AltCatStr"::: ) "st" (Bool (Bool (Set (Var "C1")) "is" ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "C2"))) & (Bool (Set (Var "C2")) "is" ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "C1")))) "holds" (Bool (Set ($#g2_altcat_1 :::"AltCatStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C1"))) "," (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "C1"))) "," (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "C1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g2_altcat_1 :::"AltCatStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C2"))) "," (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "C2"))) "," (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "C2"))) "#)" ))) ; registrationlet "C" be ($#l2_altcat_1 :::"AltCatStr"::: ) ; cluster ($#v6_altcat_1 :::"strict"::: ) for ($#m1_altcat_2 :::"SubCatStr"::: ) "of" "C"; end; definitionlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "o" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); func :::"ObCat"::: "o" -> ($#v6_altcat_1 :::"strict"::: ) ($#m1_altcat_2 :::"SubCatStr"::: ) "of" "C" means :: ALTCAT_2:def 12 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) "o" ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "(" "o" "," "o" ")" ($#k17_funcop_1 :::":->"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) "o" "," "o" ($#k1_altcat_1 :::"^>"::: ) ))) & (Bool (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_domain_1 :::"["::: ) "o" "," "o" "," "o" ($#k4_domain_1 :::"]"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" "C") ($#k4_altcat_1 :::"."::: ) "(" "o" "," "o" "," "o" ")" ")" ))) ")" ); end; :: deftheorem defines :::"ObCat"::: ALTCAT_2:def 12 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "b3")) "being" ($#v6_altcat_1 :::"strict"::: ) ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_altcat_2 :::"ObCat"::: ) (Set (Var "o")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "o")) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "o")) "," (Set (Var "o")) ")" ($#k17_funcop_1 :::":->"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "o")) ($#k1_altcat_1 :::"^>"::: ) ))) & (Bool (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_domain_1 :::"["::: ) (Set (Var "o")) "," (Set (Var "o")) "," (Set (Var "o")) ($#k4_domain_1 :::"]"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "C"))) ($#k4_altcat_1 :::"."::: ) "(" (Set (Var "o")) "," (Set (Var "o")) "," (Set (Var "o")) ")" ")" ))) ")" ) ")" )))); theorem :: ALTCAT_2:23 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "o9")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" ($#k6_altcat_2 :::"ObCat"::: ) (Set (Var "o")) ")" ) "holds" (Bool (Set (Var "o9")) ($#r1_hidden :::"="::: ) (Set (Var "o")))))) ; registrationlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "o" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); cluster (Set ($#k6_altcat_2 :::"ObCat"::: ) "o") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v6_altcat_1 :::"strict"::: ) ; end; registrationlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v6_altcat_1 :::"strict"::: ) for ($#m1_altcat_2 :::"SubCatStr"::: ) "of" "C"; end; theorem :: ALTCAT_2:24 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "D1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "D2")))) & (Bool (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "D1"))) ($#r2_altcat_2 :::"cc="::: ) (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "D2"))))) "holds" (Bool (Set (Var "D1")) "is" ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "D2"))))) ; definitionlet "C" be ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "D" be ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Const "C")); attr "D" is :::"full"::: means :: ALTCAT_2:def 13 (Bool (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" "D") ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" "C") ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "D"))); end; :: deftheorem defines :::"full"::: ALTCAT_2:def 13 : (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "D")) "is" ($#v2_altcat_2 :::"full"::: ) ) "iff" (Bool (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "C"))) ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "D"))))) ")" ))); definitionlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "D" be ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Const "C")); attr "D" is :::"id-inheriting"::: means :: ALTCAT_2:def 14 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" "D" (Bool "for" (Set (Var "o9")) "being" ($#m1_subset_1 :::"object":::) "of" "C" "st" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set (Var "o9")))) "holds" (Bool (Set ($#k8_altcat_1 :::"idm"::: ) (Set (Var "o9"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "o")) ($#k1_altcat_1 :::"^>"::: ) )))) if (Bool (Bool "not" "D" "is" ($#v2_struct_0 :::"empty"::: ) )) otherwise (Bool verum); end; :: deftheorem defines :::"id-inheriting"::: ALTCAT_2:def 14 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "C")) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "D")) "is" ($#v2_struct_0 :::"empty"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "D")) "is" ($#v3_altcat_2 :::"id-inheriting"::: ) ) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "o9")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set (Var "o9")))) "holds" (Bool (Set ($#k8_altcat_1 :::"idm"::: ) (Set (Var "o9"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "o")) ($#k1_altcat_1 :::"^>"::: ) )))) ")" ) ")" & "(" (Bool (Bool (Set (Var "D")) "is" ($#v2_struct_0 :::"empty"::: ) )) "implies" (Bool "(" (Bool (Set (Var "D")) "is" ($#v3_altcat_2 :::"id-inheriting"::: ) ) "iff" (Bool verum) ")" ) ")" ")" ))); registrationlet "C" be ($#l2_altcat_1 :::"AltCatStr"::: ) ; cluster ($#v6_altcat_1 :::"strict"::: ) ($#v2_altcat_2 :::"full"::: ) for ($#m1_altcat_2 :::"SubCatStr"::: ) "of" "C"; end; registrationlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_altcat_1 :::"strict"::: ) ($#v2_altcat_2 :::"full"::: ) for ($#m1_altcat_2 :::"SubCatStr"::: ) "of" "C"; end; registrationlet "C" be ($#l2_altcat_1 :::"category":::); let "o" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); cluster (Set ($#k6_altcat_2 :::"ObCat"::: ) "o") -> ($#v6_altcat_1 :::"strict"::: ) ($#v2_altcat_2 :::"full"::: ) ($#v3_altcat_2 :::"id-inheriting"::: ) ; end; registrationlet "C" be ($#l2_altcat_1 :::"category":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_altcat_1 :::"strict"::: ) ($#v2_altcat_2 :::"full"::: ) ($#v3_altcat_2 :::"id-inheriting"::: ) for ($#m1_altcat_2 :::"SubCatStr"::: ) "of" "C"; end; theorem :: ALTCAT_2:25 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C")))) & (Bool (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "C"))))) "holds" (Bool (Set ($#g2_altcat_1 :::"AltCatStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "D"))) "," (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "D"))) "," (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "D"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g2_altcat_1 :::"AltCatStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "C"))) "#)" )))) ; theorem :: ALTCAT_2:26 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "D1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "D2")))) & (Bool (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "D1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "D2"))))) "holds" (Bool (Set ($#g2_altcat_1 :::"AltCatStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "D1"))) "," (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "D1"))) "," (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "D1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g2_altcat_1 :::"AltCatStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "D2"))) "," (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "D2"))) "," (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "D2"))) "#)" )))) ; theorem :: ALTCAT_2:27 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#v2_altcat_2 :::"full"::: ) ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))))) "holds" (Bool (Set ($#g2_altcat_1 :::"AltCatStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "D"))) "," (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "D"))) "," (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "D"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g2_altcat_1 :::"AltCatStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "C"))) "#)" )))) ; theorem :: ALTCAT_2:28 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_2 :::"full"::: ) ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Var "p2")))) "holds" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k1_altcat_1 :::"^>"::: ) )))))) ; theorem :: ALTCAT_2:29 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "D")) "holds" (Bool (Set (Var "o")) "is" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")))))) ; registrationlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_2 :::"full"::: ) -> ($#v2_altcat_1 :::"transitive"::: ) for ($#m1_altcat_2 :::"SubCatStr"::: ) "of" "C"; end; theorem :: ALTCAT_2:30 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_2 :::"full"::: ) ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "D1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "D2"))))) "holds" (Bool (Set ($#g2_altcat_1 :::"AltCatStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "D1"))) "," (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "D1"))) "," (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "D1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g2_altcat_1 :::"AltCatStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "D2"))) "," (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "D2"))) "," (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "D2"))) "#)" )))) ; theorem :: ALTCAT_2:31 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Var "p2")))) "holds" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) )))))) ; theorem :: ALTCAT_2:32 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "p2")) "," (Set (Var "p3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Var "p2"))) & (Bool (Set (Var "o3")) ($#r1_hidden :::"="::: ) (Set (Var "p3")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) (Bool "for" (Set (Var "ff")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "p1")) "," (Set (Var "p2")) (Bool "for" (Set (Var "gg")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "p2")) "," (Set (Var "p3")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "ff"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "gg")))) "holds" (Bool (Set (Set (Var "g")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "gg")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "ff")))))))))))) ; registrationlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v11_altcat_1 :::"associative"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_altcat_1 :::"associative"::: ) for ($#m1_altcat_2 :::"SubCatStr"::: ) "of" "C"; end; theorem :: ALTCAT_2:33 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Var "p2"))) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "p1")) "," (Set (Var "p2")) "holds" (Bool (Set (Var "n")) "is" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")))))))) ; registrationlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v3_altcat_2 :::"id-inheriting"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) for ($#m1_altcat_2 :::"SubCatStr"::: ) "of" "C"; end; registrationlet "C" be ($#l2_altcat_1 :::"category":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v3_altcat_2 :::"id-inheriting"::: ) for ($#m1_altcat_2 :::"SubCatStr"::: ) "of" "C"; end; definitionlet "C" be ($#l2_altcat_1 :::"category":::); mode subcategory of "C" is ($#v2_altcat_1 :::"transitive"::: ) ($#v3_altcat_2 :::"id-inheriting"::: ) ($#m1_altcat_2 :::"SubCatStr"::: ) "of" "C"; end; theorem :: ALTCAT_2:34 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "D")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "o9")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set (Var "o9")))) "holds" (Bool (Set ($#k8_altcat_1 :::"idm"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k8_altcat_1 :::"idm"::: ) (Set (Var "o9")))))))) ;