:: YELLOW20 semantic presentation begin theorem :: YELLOW20:1 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v6_functor0 :::"reflexive"::: ) ($#v8_functor0 :::"feasible"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v7_functor0 :::"coreflexive"::: ) ) & (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) )) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) "iff" (Bool (Set (Set "(" (Set (Var "F")) ($#k15_functor0 :::"""::: ) ")" ) ($#k3_functor0 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))))) ; theorem :: YELLOW20:2 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v8_functor0 :::"feasible"::: ) ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#v8_functor0 :::"feasible"::: ) ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) ))) "holds" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a1")) "," (Set (Var "a2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "a1")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "a2")) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k6_functor0 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) "iff" (Bool (Set (Set (Var "G")) ($#k6_functor0 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ))))))) ; theorem :: YELLOW20:3 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v8_functor0 :::"feasible"::: ) ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#v8_functor0 :::"feasible"::: ) ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) ))) "holds" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a1")) "," (Set (Var "a2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "a2")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "a1")) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k8_functor0 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) "iff" (Bool (Set (Set (Var "G")) ($#k8_functor0 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ))))))) ; theorem :: YELLOW20:4 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) )) "holds" (Bool "for" (Set (Var "G")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "F")) ($#k13_functor0 :::"*"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k12_functor0 :::"id"::: ) (Set (Var "B"))))) "holds" (Bool (Set ($#g2_functor0 :::"FunctorStr"::: ) "(#" (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" (Set (Var "G"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) ))))) ; theorem :: YELLOW20:5 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) )) "holds" (Bool "for" (Set (Var "G")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "G")) ($#k13_functor0 :::"*"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k12_functor0 :::"id"::: ) (Set (Var "A"))))) "holds" (Bool (Set ($#g2_functor0 :::"FunctorStr"::: ) "(#" (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" (Set (Var "G"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) ))))) ; theorem :: YELLOW20:6 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) )) "holds" (Bool "for" (Set (Var "G")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B")) "holds" (Bool (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set "(" (Set (Var "G")) ($#k3_functor0 :::"."::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set (Var "F")) ($#k6_functor0 :::"."::: ) (Set "(" (Set (Var "G")) ($#k6_functor0 :::"."::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f")))) ")" )) "holds" (Bool (Set ($#g2_functor0 :::"FunctorStr"::: ) "(#" (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" (Set (Var "G"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) ))))) ; theorem :: YELLOW20:7 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) )) "holds" (Bool "for" (Set (Var "G")) "being" ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B")) "holds" (Bool (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set "(" (Set (Var "G")) ($#k3_functor0 :::"."::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set (Var "F")) ($#k8_functor0 :::"."::: ) (Set "(" (Set (Var "G")) ($#k8_functor0 :::"."::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f")))) ")" )) "holds" (Bool (Set ($#g2_functor0 :::"FunctorStr"::: ) "(#" (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" (Set (Var "G"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) ))))) ; theorem :: YELLOW20:8 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) )) "holds" (Bool "for" (Set (Var "G")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "G")) ($#k3_functor0 :::"."::: ) (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set (Var "G")) ($#k6_functor0 :::"."::: ) (Set "(" (Set (Var "F")) ($#k6_functor0 :::"."::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f")))) ")" )) "holds" (Bool (Set ($#g2_functor0 :::"FunctorStr"::: ) "(#" (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" (Set (Var "G"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) ))))) ; theorem :: YELLOW20:9 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) )) "holds" (Bool "for" (Set (Var "G")) "being" ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "G")) ($#k3_functor0 :::"."::: ) (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set (Var "G")) ($#k8_functor0 :::"."::: ) (Set "(" (Set (Var "F")) ($#k8_functor0 :::"."::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f")))) ")" )) "holds" (Bool (Set ($#g2_functor0 :::"FunctorStr"::: ) "(#" (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" (Set (Var "G"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) ))))) ; begin definitionlet "A", "B" be ($#l2_altcat_1 :::"AltCatStr"::: ) ; pred "A" "," "B" :::"have_the_same_composition"::: means :: YELLOW20:def 1 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" "A") ($#k1_funct_1 :::"."::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k3_xtuple_0 :::"]"::: ) )) ($#r1_partfun1 :::"tolerates"::: ) (Set (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" "B") ($#k1_funct_1 :::"."::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k3_xtuple_0 :::"]"::: ) )))); symmetry (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"AltCatStr"::: ) "st" (Bool (Bool "(" "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k3_xtuple_0 :::"]"::: ) )) ($#r1_partfun1 :::"tolerates"::: ) (Set (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "B"))) ($#k1_funct_1 :::"."::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k3_xtuple_0 :::"]"::: ) ))) ")" )) "holds" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "B"))) ($#k1_funct_1 :::"."::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k3_xtuple_0 :::"]"::: ) )) ($#r1_partfun1 :::"tolerates"::: ) (Set (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k3_xtuple_0 :::"]"::: ) ))))) ; end; :: deftheorem defines :::"have_the_same_composition"::: YELLOW20:def 1 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"AltCatStr"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_yellow20 :::"have_the_same_composition"::: ) ) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k3_xtuple_0 :::"]"::: ) )) ($#r1_partfun1 :::"tolerates"::: ) (Set (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "B"))) ($#k1_funct_1 :::"."::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k3_xtuple_0 :::"]"::: ) )))) ")" )); theorem :: YELLOW20:10 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"AltCatStr"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_yellow20 :::"have_the_same_composition"::: ) ) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k3_xtuple_0 :::"]"::: ) ) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "B"))) ($#k1_funct_1 :::"."::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k3_xtuple_0 :::"]"::: ) ) ")" )))) "holds" (Bool (Set (Set "(" (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k3_xtuple_0 :::"]"::: ) ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "B"))) ($#k1_funct_1 :::"."::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k3_xtuple_0 :::"]"::: ) ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) ")" )) ; theorem :: YELLOW20:11 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_yellow20 :::"have_the_same_composition"::: ) ) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a2")) "," (Set (Var "a3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b1")) "," (Set (Var "b2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b2")) "," (Set (Var "b3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "a1"))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Var "a3")))) "holds" (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a1")) "," (Set (Var "a2")) (Bool "for" (Set (Var "g1")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b1")) "," (Set (Var "b2")) "st" (Bool (Bool (Set (Var "g1")) ($#r1_hidden :::"="::: ) (Set (Var "f1")))) "holds" (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a2")) "," (Set (Var "a3")) (Bool "for" (Set (Var "g2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b2")) "," (Set (Var "b3")) "st" (Bool (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Var "f2")))) "holds" (Bool (Set (Set (Var "f2")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g2")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "g1")))))))))) ")" )) ; theorem :: YELLOW20:12 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v9_altcat_1 :::"semi-functional"::: ) ($#v2_yellow18 :::"para-functional"::: ) ($#l2_altcat_1 :::"category":::) "holds" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_yellow20 :::"have_the_same_composition"::: ) )) ; definitionlet "f", "g" be ($#m1_hidden :::"Function":::); func :::"Intersect"::: "(" "f" "," "g" ")" -> ($#m1_hidden :::"Function":::) means :: YELLOW20:def 2 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" )))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" "g" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" )))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" )) ; end; :: deftheorem defines :::"Intersect"::: YELLOW20:def 2 : (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow20 :::"Intersect"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" )) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" )))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" )); theorem :: YELLOW20:13 (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 (Set ($#k1_yellow20 :::"Intersect"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_pboole :::"/\"::: ) (Set (Var "B")))))) ; theorem :: YELLOW20:14 (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 (Set ($#k1_yellow20 :::"Intersect"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) "is" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Set (Var "I")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "J"))))))) ; theorem :: YELLOW20:15 (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 :::"Function":::) (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) "st" (Bool (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow20 :::"Intersect"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ))) "holds" (Bool (Set (Var "C")) ($#r2_altcat_2 :::"cc="::: ) (Set (Var "A"))))))) ; theorem :: YELLOW20:16 (Bool "for" (Set (Var "I1")) "," (Set (Var "I2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "B1")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I1")) (Bool "for" (Set (Var "A2")) "," (Set (Var "B2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I2")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Set (Var "I1")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "I2"))) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow20 :::"Intersect"::: ) "(" (Set (Var "A1")) "," (Set (Var "A2")) ")" )) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow20 :::"Intersect"::: ) "(" (Set (Var "B1")) "," (Set (Var "B2")) ")" ))) "holds" (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A1")) "," (Set (Var "B1")) (Bool "for" (Set (Var "G")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A2")) "," (Set (Var "B2")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_partfun1 :::"tolerates"::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set ($#k1_yellow20 :::"Intersect"::: ) "(" (Set (Var "F")) "," (Set (Var "G")) ")" ) "is" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B"))))))))) ; theorem :: YELLOW20:17 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "I")) "," (Set (Var "I")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "J")) "," (Set (Var "J")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "ex" (Set (Var "H")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set (Var "I")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "J")) ")" ) "," (Set "(" (Set (Var "I")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "J")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool "(" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow20 :::"Intersect"::: ) "(" (Set (Var "F")) "," (Set (Var "G")) ")" )) & (Bool (Set ($#k1_yellow20 :::"Intersect"::: ) "(" (Set ($#k2_altcat_1 :::"{|"::: ) (Set (Var "F")) ($#k2_altcat_1 :::"|}"::: ) ) "," (Set ($#k2_altcat_1 :::"{|"::: ) (Set (Var "G")) ($#k2_altcat_1 :::"|}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_altcat_1 :::"{|"::: ) (Set (Var "H")) ($#k2_altcat_1 :::"|}"::: ) )) ")" ))))) ; theorem :: YELLOW20:18 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "I")) "," (Set (Var "I")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "J")) "," (Set (Var "J")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "ex" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set (Var "I")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "J")) ")" ) "," (Set "(" (Set (Var "I")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "J")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool "(" (Bool (Set (Var "H1")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow20 :::"Intersect"::: ) "(" (Set (Var "F1")) "," (Set (Var "G1")) ")" )) & (Bool (Set (Var "H2")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow20 :::"Intersect"::: ) "(" (Set (Var "F2")) "," (Set (Var "G2")) ")" )) & (Bool (Set ($#k1_yellow20 :::"Intersect"::: ) "(" (Set ($#k3_altcat_1 :::"{|"::: ) (Set (Var "F1")) "," (Set (Var "F2")) ($#k3_altcat_1 :::"|}"::: ) ) "," (Set ($#k3_altcat_1 :::"{|"::: ) (Set (Var "G1")) "," (Set (Var "G2")) ($#k3_altcat_1 :::"|}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_altcat_1 :::"{|"::: ) (Set (Var "H1")) "," (Set (Var "H2")) ($#k3_altcat_1 :::"|}"::: ) )) ")" ))))) ; definitionlet "A", "B" be ($#l2_altcat_1 :::"AltCatStr"::: ) ; assume (Bool (Set (Const "A")) "," (Set (Const "B")) ($#r1_yellow20 :::"have_the_same_composition"::: ) ) ; func :::"Intersect"::: "(" "A" "," "B" ")" -> ($#v6_altcat_1 :::"strict"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) means :: YELLOW20:def 3 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "B"))) & (Bool (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow20 :::"Intersect"::: ) "(" (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" "A") "," (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" "B") ")" )) & (Bool (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow20 :::"Intersect"::: ) "(" (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" "A") "," (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" "B") ")" )) ")" ); end; :: deftheorem defines :::"Intersect"::: YELLOW20:def 3 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"AltCatStr"::: ) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_yellow20 :::"have_the_same_composition"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#v6_altcat_1 :::"strict"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow20 :::"Intersect"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "B"))))) & (Bool (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow20 :::"Intersect"::: ) "(" (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "B"))) ")" )) & (Bool (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow20 :::"Intersect"::: ) "(" (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "B"))) ")" )) ")" ) ")" ))); theorem :: YELLOW20:19 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"AltCatStr"::: ) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_yellow20 :::"have_the_same_composition"::: ) )) "holds" (Bool (Set ($#k2_yellow20 :::"Intersect"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow20 :::"Intersect"::: ) "(" (Set (Var "B")) "," (Set (Var "A")) ")" ))) ; theorem :: YELLOW20:20 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"AltCatStr"::: ) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_yellow20 :::"have_the_same_composition"::: ) )) "holds" (Bool (Set ($#k2_yellow20 :::"Intersect"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) "is" ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "A")))) ; theorem :: YELLOW20:21 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"AltCatStr"::: ) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_yellow20 :::"have_the_same_composition"::: ) )) "holds" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" ($#k2_yellow20 :::"Intersect"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) "st" (Bool (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Var "a1"))) & (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Var "b1"))) & (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Var "b2")))) "holds" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#k3_xboole_0 :::"/\"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b1")) "," (Set (Var "b2")) ($#k1_altcat_1 :::"^>"::: ) ))))))) ; theorem :: YELLOW20:22 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_yellow20 :::"have_the_same_composition"::: ) )) "holds" (Bool (Set ($#k2_yellow20 :::"Intersect"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) "is" ($#v2_altcat_1 :::"transitive"::: ) )) ; theorem :: YELLOW20:23 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"AltCatStr"::: ) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_yellow20 :::"have_the_same_composition"::: ) )) "holds" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" ($#k2_yellow20 :::"Intersect"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) "st" (Bool (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Var "a1"))) & (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Var "b1"))) & (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b1")) "," (Set (Var "b2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a1")) "," (Set (Var "a2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b1")) "," (Set (Var "b2")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) )))))))) ; theorem :: YELLOW20:24 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_yellow20 :::"have_the_same_composition"::: ) )) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" ($#k2_yellow20 :::"Intersect"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) "st" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k8_altcat_1 :::"idm"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k8_altcat_1 :::"idm"::: ) (Set (Var "b"))))) "holds" (Bool (Set ($#k8_altcat_1 :::"idm"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "o")) ($#k1_altcat_1 :::"^>"::: ) )))))) ; theorem :: YELLOW20:25 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_yellow20 :::"have_the_same_composition"::: ) ) & (Bool (Bool "not" (Set ($#k2_yellow20 :::"Intersect"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) "is" ($#v2_struct_0 :::"empty"::: ) )) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k8_altcat_1 :::"idm"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k8_altcat_1 :::"idm"::: ) (Set (Var "b"))))) ")" )) "holds" (Bool (Set ($#k2_yellow20 :::"Intersect"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) "is" ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A")))) ; begin scheme :: YELLOW20:sch 1 SubcategoryUniq{ F1() -> ($#l2_altcat_1 :::"category":::), F2() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set F1 "(" ")" ), F3() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool (Set ($#g2_altcat_1 :::"AltCatStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F2 "(" ")" )) "," (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set F2 "(" ")" )) "," (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set F2 "(" ")" )) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g2_altcat_1 :::"AltCatStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F3 "(" ")" )) "," (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set F3 "(" ")" )) "," (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set F3 "(" ")" )) "#)" )) provided (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"object":::) "of" (Set F2 "(" ")" )) "iff" (Bool P1[(Set (Var "a"))]) ")" )) and (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"object":::) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "b9")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a9")) "," (Set (Var "b9")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool P2[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))]) ")" )))) and (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"object":::) "of" (Set F3 "(" ")" )) "iff" (Bool P1[(Set (Var "a"))]) ")" )) and (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"object":::) "of" (Set F3 "(" ")" ) "st" (Bool (Bool (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "b9")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a9")) "," (Set (Var "b9")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool P2[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))]) ")" )))) proof end; theorem :: YELLOW20:26 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v2_altcat_2 :::"full"::: ) ) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "a1"))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "a2")))) "holds" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b1")) "," (Set (Var "b2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k1_altcat_1 :::"^>"::: ) )))) ")" ))) ; scheme :: YELLOW20:sch 2 FullSubcategoryEx{ F1() -> ($#l2_altcat_1 :::"category":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_altcat_1 :::"strict"::: ) ($#v2_altcat_2 :::"full"::: ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B"))) "iff" (Bool P1[(Set (Var "a"))]) ")" ))) provided (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set F1 "(" ")" ) "st" (Bool P1[(Set (Var "a"))])) proof end; scheme :: YELLOW20:sch 3 FullSubcategoryUniq{ F1() -> ($#l2_altcat_1 :::"category":::), F2() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_2 :::"full"::: ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set F1 "(" ")" ), F3() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_2 :::"full"::: ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool (Set ($#g2_altcat_1 :::"AltCatStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F2 "(" ")" )) "," (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set F2 "(" ")" )) "," (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set F2 "(" ")" )) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g2_altcat_1 :::"AltCatStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F3 "(" ")" )) "," (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set F3 "(" ")" )) "," (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set F3 "(" ")" )) "#)" )) provided (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"object":::) "of" (Set F2 "(" ")" )) "iff" (Bool P1[(Set (Var "a"))]) ")" )) and (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"object":::) "of" (Set F3 "(" ")" )) "iff" (Bool P1[(Set (Var "a"))]) ")" )) proof end; begin registrationlet "f" be ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::); let "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k1_binop_1 :::"."::: ) "(" "x" "," "y" ")" ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; theorem :: YELLOW20:27 (Bool "for" (Set (Var "A")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set "(" ($#k10_functor0 :::"incl"::: ) (Set (Var "C")) ")" ) ($#k6_functor0 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))))))) ; registrationlet "A" be ($#l2_altcat_1 :::"category":::); let "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Const "A")); cluster (Set ($#k10_functor0 :::"incl"::: ) "C") -> ($#v12_functor0 :::"id-preserving"::: ) ($#v13_functor0 :::"comp-preserving"::: ) ; end; registrationlet "A" be ($#l2_altcat_1 :::"category":::); let "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Const "A")); cluster (Set ($#k10_functor0 :::"incl"::: ) "C") -> ($#v10_functor0 :::"Covariant"::: ) ; end; definitionlet "A" be ($#l2_altcat_1 :::"category":::); let "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Const "A")); :: original: :::"incl"::: redefine func :::"incl"::: "C" -> ($#v9_functor0 :::"strict"::: ) ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" "C" "," "A"; end; definitionlet "A", "B" be ($#l2_altcat_1 :::"category":::); let "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Const "A")); let "F" be ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); :: original: :::"|"::: redefine func "F" :::"|"::: "C" -> ($#v9_functor0 :::"strict"::: ) ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" "C" "," "B"; end; definitionlet "A", "B" be ($#l2_altcat_1 :::"category":::); let "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Const "A")); let "F" be ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); :: original: :::"|"::: redefine func "F" :::"|"::: "C" -> ($#v9_functor0 :::"strict"::: ) ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" "C" "," "B"; end; theorem :: YELLOW20:28 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "F")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k14_functor0 :::"|"::: ) (Set (Var "C")) ")" ) ($#k3_functor0 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "a"))))))))) ; theorem :: YELLOW20:29 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "F")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "c")) "," (Set (Var "d")) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "f")))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k4_yellow20 :::"|"::: ) (Set (Var "C")) ")" ) ($#k6_functor0 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k6_functor0 :::"."::: ) (Set (Var "f"))))))))))) ; theorem :: YELLOW20:30 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "F")) "being" ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "c")) "," (Set (Var "d")) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "f")))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k5_yellow20 :::"|"::: ) (Set (Var "C")) ")" ) ($#k8_functor0 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_functor0 :::"."::: ) (Set (Var "f"))))))))))) ; theorem :: YELLOW20:31 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#l1_functor0 :::"BimapStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v10_functor0 :::"Covariant"::: ) ) & (Bool (Set (Var "F")) "is" ($#v4_functor0 :::"one-to-one"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))))) ; theorem :: YELLOW20:32 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#v8_functor0 :::"feasible"::: ) ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v17_functor0 :::"faithful"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set (Set (Var "F")) ($#k6_functor0 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k6_functor0 :::"."::: ) (Set (Var "g"))))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))))))) ; theorem :: YELLOW20:33 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v20_functor0 :::"surjective"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "ex" (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A"))(Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "c")) "," (Set (Var "d")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "c")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "d")))) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k6_functor0 :::"."::: ) (Set (Var "g")))) ")" ))))))) ; theorem :: YELLOW20:34 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#l1_functor0 :::"BimapStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v11_functor0 :::"Contravariant"::: ) ) & (Bool (Set (Var "F")) "is" ($#v4_functor0 :::"one-to-one"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))))) ; theorem :: YELLOW20:35 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#v8_functor0 :::"feasible"::: ) ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v17_functor0 :::"faithful"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set (Set (Var "F")) ($#k8_functor0 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_functor0 :::"."::: ) (Set (Var "g"))))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))))))) ; theorem :: YELLOW20:36 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v20_functor0 :::"surjective"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "ex" (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A"))(Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "c")) "," (Set (Var "d")) "st" (Bool "(" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "c")))) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "d")))) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_functor0 :::"."::: ) (Set (Var "g")))) ")" ))))))) ; begin definitionlet "A", "B" be ($#l2_altcat_1 :::"category":::); let "F" be ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "A")) "," (Set (Const "B")); let "A9", "B9" be ($#l2_altcat_1 :::"category":::); pred "A9" "," "B9" :::"are_isomorphic_under"::: "F" means :: YELLOW20:def 4 (Bool "(" (Bool "A9" "is" ($#m1_altcat_2 :::"subcategory":::) "of" "A") & (Bool "B9" "is" ($#m1_altcat_2 :::"subcategory":::) "of" "B") & (Bool "ex" (Set (Var "G")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" "A9" "," "B9" "st" (Bool "(" (Bool (Set (Var "G")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool "(" "for" (Set (Var "a9")) "being" ($#m1_subset_1 :::"object":::) "of" "A9" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" "A" "st" (Bool (Bool (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "G")) ($#k3_functor0 :::"."::: ) (Set (Var "a9"))) ($#r1_hidden :::"="::: ) (Set "F" ($#k3_functor0 :::"."::: ) (Set (Var "a"))))) ")" ) & (Bool "(" "for" (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"object":::) "of" "A9" (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"object":::) "of" "A" "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b9")) "," (Set (Var "c9")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "b9")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "c9")) ($#r1_hidden :::"="::: ) (Set (Var "c")))) "holds" (Bool "for" (Set (Var "f9")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b9")) "," (Set (Var "c9")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b")) "," (Set (Var "c")) "st" (Bool (Bool (Set (Var "f9")) ($#r1_hidden :::"="::: ) (Set (Var "f")))) "holds" (Bool (Set (Set (Var "G")) ($#k6_functor0 :::"."::: ) (Set (Var "f9"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" "F" "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))))))) ")" ) ")" )) ")" ); pred "A9" "," "B9" :::"are_anti-isomorphic_under"::: "F" means :: YELLOW20:def 5 (Bool "(" (Bool "A9" "is" ($#m1_altcat_2 :::"subcategory":::) "of" "A") & (Bool "B9" "is" ($#m1_altcat_2 :::"subcategory":::) "of" "B") & (Bool "ex" (Set (Var "G")) "being" ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" "A9" "," "B9" "st" (Bool "(" (Bool (Set (Var "G")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool "(" "for" (Set (Var "a9")) "being" ($#m1_subset_1 :::"object":::) "of" "A9" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" "A" "st" (Bool (Bool (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "G")) ($#k3_functor0 :::"."::: ) (Set (Var "a9"))) ($#r1_hidden :::"="::: ) (Set "F" ($#k3_functor0 :::"."::: ) (Set (Var "a"))))) ")" ) & (Bool "(" "for" (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"object":::) "of" "A9" (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"object":::) "of" "A" "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b9")) "," (Set (Var "c9")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "b9")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "c9")) ($#r1_hidden :::"="::: ) (Set (Var "c")))) "holds" (Bool "for" (Set (Var "f9")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b9")) "," (Set (Var "c9")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b")) "," (Set (Var "c")) "st" (Bool (Bool (Set (Var "f9")) ($#r1_hidden :::"="::: ) (Set (Var "f")))) "holds" (Bool (Set (Set (Var "G")) ($#k8_functor0 :::"."::: ) (Set (Var "f9"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" "F" "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))))))) ")" ) ")" )) ")" ); end; :: deftheorem defines :::"are_isomorphic_under"::: YELLOW20:def 4 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#l2_altcat_1 :::"category":::) "holds" (Bool "(" (Bool (Set (Var "A9")) "," (Set (Var "B9")) ($#r2_yellow20 :::"are_isomorphic_under"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "A9")) "is" ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A"))) & (Bool (Set (Var "B9")) "is" ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "B"))) & (Bool "ex" (Set (Var "G")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A9")) "," (Set (Var "B9")) "st" (Bool "(" (Bool (Set (Var "G")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool "(" "for" (Set (Var "a9")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A9")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "G")) ($#k3_functor0 :::"."::: ) (Set (Var "a9"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "a"))))) ")" ) & (Bool "(" "for" (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A9")) (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b9")) "," (Set (Var "c9")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "b9")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "c9")) ($#r1_hidden :::"="::: ) (Set (Var "c")))) "holds" (Bool "for" (Set (Var "f9")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b9")) "," (Set (Var "c9")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b")) "," (Set (Var "c")) "st" (Bool (Bool (Set (Var "f9")) ($#r1_hidden :::"="::: ) (Set (Var "f")))) "holds" (Bool (Set (Set (Var "G")) ($#k6_functor0 :::"."::: ) (Set (Var "f9"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set (Var "F")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))))))) ")" ) ")" )) ")" ) ")" )))); :: deftheorem defines :::"are_anti-isomorphic_under"::: YELLOW20:def 5 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#l2_altcat_1 :::"category":::) "holds" (Bool "(" (Bool (Set (Var "A9")) "," (Set (Var "B9")) ($#r3_yellow20 :::"are_anti-isomorphic_under"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "A9")) "is" ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A"))) & (Bool (Set (Var "B9")) "is" ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "B"))) & (Bool "ex" (Set (Var "G")) "being" ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A9")) "," (Set (Var "B9")) "st" (Bool "(" (Bool (Set (Var "G")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool "(" "for" (Set (Var "a9")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A9")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "G")) ($#k3_functor0 :::"."::: ) (Set (Var "a9"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "a"))))) ")" ) & (Bool "(" "for" (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A9")) (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b9")) "," (Set (Var "c9")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "b9")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "c9")) ($#r1_hidden :::"="::: ) (Set (Var "c")))) "holds" (Bool "for" (Set (Var "f9")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b9")) "," (Set (Var "c9")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b")) "," (Set (Var "c")) "st" (Bool (Bool (Set (Var "f9")) ($#r1_hidden :::"="::: ) (Set (Var "f")))) "holds" (Bool (Set (Set (Var "G")) ($#k8_functor0 :::"."::: ) (Set (Var "f9"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set (Var "F")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))))))) ")" ) ")" )) ")" ) ")" )))); theorem :: YELLOW20:37 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "A1")) "," (Set (Var "B1")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "B1")) ($#r2_yellow20 :::"are_isomorphic_under"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "A1")) "," (Set (Var "B1")) ($#r1_functor0 :::"are_isomorphic"::: ) ))) ; theorem :: YELLOW20:38 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "A1")) "," (Set (Var "B1")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "B1")) ($#r3_yellow20 :::"are_anti-isomorphic_under"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "A1")) "," (Set (Var "B1")) ($#r2_functor0 :::"are_anti-isomorphic"::: ) ))) ; theorem :: YELLOW20:39 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r2_yellow20 :::"are_isomorphic_under"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ))) ; theorem :: YELLOW20:40 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r3_yellow20 :::"are_anti-isomorphic_under"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ))) ; theorem :: YELLOW20:41 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) )) "holds" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r2_yellow20 :::"are_isomorphic_under"::: ) (Set (Var "F"))))) ; theorem :: YELLOW20:42 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) )) "holds" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r3_yellow20 :::"are_anti-isomorphic_under"::: ) (Set (Var "F"))))) ; theorem :: YELLOW20:43 (Bool "for" (Set (Var "A")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A")) "holds" (Bool (Set (Var "B")) "," (Set (Var "B")) ($#r2_yellow20 :::"are_isomorphic_under"::: ) (Set ($#k12_functor0 :::"id"::: ) (Set (Var "A")))))) ; theorem :: YELLOW20:44 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Var "g")))) "holds" (Bool (Set ($#k2_funct_4 :::"~"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_funct_4 :::"~"::: ) (Set (Var "g"))))) ; theorem :: YELLOW20:45 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) "is" ($#m1_hidden :::"Relation":::)) & (Bool (Set ($#k2_funct_4 :::"~"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_funct_4 :::"~"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Var "g")))) ; theorem :: YELLOW20:46 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "I")) "," (Set (Var "I")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "J")) "," (Set (Var "J")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r2_altcat_2 :::"cc="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_funct_4 :::"~"::: ) (Set (Var "A"))) ($#r2_altcat_2 :::"cc="::: ) (Set ($#k2_funct_4 :::"~"::: ) (Set (Var "B"))))))) ; theorem :: YELLOW20:47 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "B")) ($#k1_yellow18 :::"opp"::: ) ) "is" ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Set (Var "A")) ($#k1_yellow18 :::"opp"::: ) )))) ; theorem :: YELLOW20:48 (Bool "for" (Set (Var "A")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "B")) ($#k1_yellow18 :::"opp"::: ) ) "is" ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Set (Var "A")) ($#k1_yellow18 :::"opp"::: ) )))) ; theorem :: YELLOW20:49 (Bool "for" (Set (Var "A")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A")) "holds" (Bool (Set (Var "B")) "," (Set (Set (Var "B")) ($#k1_yellow18 :::"opp"::: ) ) ($#r3_yellow20 :::"are_anti-isomorphic_under"::: ) (Set ($#k2_yellow18 :::"dualizing-func"::: ) "(" (Set (Var "A")) "," (Set "(" (Set (Var "A")) ($#k1_yellow18 :::"opp"::: ) ")" ) ")" )))) ; theorem :: YELLOW20:50 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A1")) "," (Set (Var "A2")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) )) "holds" (Bool "for" (Set (Var "B1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A1")) (Bool "for" (Set (Var "B2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "B1")) "," (Set (Var "B2")) ($#r2_yellow20 :::"are_isomorphic_under"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "B2")) "," (Set (Var "B1")) ($#r2_yellow20 :::"are_isomorphic_under"::: ) (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) )))))) ; theorem :: YELLOW20:51 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A1")) "," (Set (Var "A2")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) )) "holds" (Bool "for" (Set (Var "B1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A1")) (Bool "for" (Set (Var "B2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "B1")) "," (Set (Var "B2")) ($#r3_yellow20 :::"are_anti-isomorphic_under"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "B2")) "," (Set (Var "B1")) ($#r3_yellow20 :::"are_anti-isomorphic_under"::: ) (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) )))))) ; theorem :: YELLOW20:52 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A1")) "," (Set (Var "A2")) (Bool "for" (Set (Var "G")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A2")) "," (Set (Var "A3")) (Bool "for" (Set (Var "B1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A1")) (Bool "for" (Set (Var "B2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A2")) (Bool "for" (Set (Var "B3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A3")) "st" (Bool (Bool (Set (Var "B1")) "," (Set (Var "B2")) ($#r2_yellow20 :::"are_isomorphic_under"::: ) (Set (Var "F"))) & (Bool (Set (Var "B2")) "," (Set (Var "B3")) ($#r2_yellow20 :::"are_isomorphic_under"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "B1")) "," (Set (Var "B3")) ($#r2_yellow20 :::"are_isomorphic_under"::: ) (Set (Set (Var "G")) ($#k1_functor3 :::"*"::: ) (Set (Var "F")))))))))) ; theorem :: YELLOW20:53 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A1")) "," (Set (Var "A2")) (Bool "for" (Set (Var "G")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A2")) "," (Set (Var "A3")) (Bool "for" (Set (Var "B1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A1")) (Bool "for" (Set (Var "B2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A2")) (Bool "for" (Set (Var "B3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A3")) "st" (Bool (Bool (Set (Var "B1")) "," (Set (Var "B2")) ($#r3_yellow20 :::"are_anti-isomorphic_under"::: ) (Set (Var "F"))) & (Bool (Set (Var "B2")) "," (Set (Var "B3")) ($#r2_yellow20 :::"are_isomorphic_under"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "B1")) "," (Set (Var "B3")) ($#r3_yellow20 :::"are_anti-isomorphic_under"::: ) (Set (Set (Var "G")) ($#k4_functor3 :::"*"::: ) (Set (Var "F")))))))))) ; theorem :: YELLOW20:54 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A1")) "," (Set (Var "A2")) (Bool "for" (Set (Var "G")) "being" ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A2")) "," (Set (Var "A3")) (Bool "for" (Set (Var "B1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A1")) (Bool "for" (Set (Var "B2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A2")) (Bool "for" (Set (Var "B3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A3")) "st" (Bool (Bool (Set (Var "B1")) "," (Set (Var "B2")) ($#r2_yellow20 :::"are_isomorphic_under"::: ) (Set (Var "F"))) & (Bool (Set (Var "B2")) "," (Set (Var "B3")) ($#r3_yellow20 :::"are_anti-isomorphic_under"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "B1")) "," (Set (Var "B3")) ($#r3_yellow20 :::"are_anti-isomorphic_under"::: ) (Set (Set (Var "G")) ($#k3_functor3 :::"*"::: ) (Set (Var "F")))))))))) ; theorem :: YELLOW20:55 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A1")) "," (Set (Var "A2")) (Bool "for" (Set (Var "G")) "being" ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A2")) "," (Set (Var "A3")) (Bool "for" (Set (Var "B1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A1")) (Bool "for" (Set (Var "B2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A2")) (Bool "for" (Set (Var "B3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A3")) "st" (Bool (Bool (Set (Var "B1")) "," (Set (Var "B2")) ($#r3_yellow20 :::"are_anti-isomorphic_under"::: ) (Set (Var "F"))) & (Bool (Set (Var "B2")) "," (Set (Var "B3")) ($#r3_yellow20 :::"are_anti-isomorphic_under"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "B1")) "," (Set (Var "B3")) ($#r2_yellow20 :::"are_isomorphic_under"::: ) (Set (Set (Var "G")) ($#k2_functor3 :::"*"::: ) (Set (Var "F")))))))))) ; theorem :: YELLOW20:56 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A1")) "," (Set (Var "A2")) (Bool "for" (Set (Var "B1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A1")) (Bool "for" (Set (Var "B2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A1")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B1"))) "iff" (Bool (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "a"))) "is" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B2"))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A1")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B1")) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool "for" (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B2")) "st" (Bool (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "b"))))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a1")) "," (Set (Var "b1")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool (Set (Set (Var "F")) ($#k6_functor0 :::"."::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a2")) "," (Set (Var "b2")) ($#k1_altcat_1 :::"^>"::: ) )) ")" )))) ")" )) "holds" (Bool (Set (Var "B1")) "," (Set (Var "B2")) ($#r2_yellow20 :::"are_isomorphic_under"::: ) (Set (Var "F"))))))) ; theorem :: YELLOW20:57 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "being" ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A1")) "," (Set (Var "A2")) (Bool "for" (Set (Var "B1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A1")) (Bool "for" (Set (Var "B2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A1")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B1"))) "iff" (Bool (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "a"))) "is" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B2"))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A1")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B1")) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool "for" (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B2")) "st" (Bool (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "b"))))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a1")) "," (Set (Var "b1")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool (Set (Set (Var "F")) ($#k8_functor0 :::"."::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b2")) "," (Set (Var "a2")) ($#k1_altcat_1 :::"^>"::: ) )) ")" )))) ")" )) "holds" (Bool (Set (Var "B1")) "," (Set (Var "B2")) ($#r3_yellow20 :::"are_anti-isomorphic_under"::: ) (Set (Var "F"))))))) ;