:: YELLOW18  semantic presentation begin  scheme  :: YELLOW18:sch 1 AltCatStrLambda{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F3(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "ex" (Set (Var "C")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#v6_altcat_1 :::"strict"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )   "st"  (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds"  (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "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 :::"{}"::: )  )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#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 "b")) "," (Set (Var "c")) "holds"  (Bool (Set (Set (Var "g"))  ($#k5_altcat_1 :::"*"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ))))  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "b")) "," (Set (Var "c")) ")" ))) "holds"  (Bool (Set F3 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "c")) ")" ))))
 proof 


end; scheme  :: YELLOW18:sch 2 CatAssocSch{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )  , F2(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool (Set F1 "("  ")" ) "is"   ($#v11_altcat_1 :::"associative"::: )  )
 provided
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#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 "b")) "," (Set (Var "c")) "holds"  (Bool (Set (Set (Var "g"))  ($#k5_altcat_1 :::"*"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "g")) ")" )))))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) & (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k1_altcat_1 :::"^>"::: ) )) & (Bool (Set (Var "h"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_altcat_1 :::"^>"::: ) ))) "holds"  (Bool (Set F2 "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ) "," (Set (Var "h")) ")" )  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "f")) "," (Set F2 "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "g")) "," (Set (Var "h")) ")" ) ")" ))))
 proof 


end; scheme  :: YELLOW18:sch 3 CatUnitsSch{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )  , F2(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool (Set F1 "("  ")" ) "is"   ($#v12_altcat_1 :::"with_units"::: )  )
 provided
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#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 "b")) "," (Set (Var "c")) "holds"  (Bool (Set (Set (Var "g"))  ($#k5_altcat_1 :::"*"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "g")) ")" )))))
 and  
(Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" ) (Bool  "ex" (Set (Var "f")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "a")) ($#k1_altcat_1 :::"^>"::: ) )) & (Bool  "("   "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "g")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ))) "holds"  (Bool (Set F2 "(" (Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "g"))))  ")" )  ")" )))
 and  
(Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" ) (Bool  "ex" (Set (Var "f")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "a")) ($#k1_altcat_1 :::"^>"::: ) )) & (Bool  "("   "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "g")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k1_altcat_1 :::"^>"::: ) ))) "holds"  (Bool (Set F2 "(" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "g")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "g"))))  ")" )  ")" )))
 proof 


end; scheme  :: YELLOW18:sch 4 CategoryLambda{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F3(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "ex" (Set (Var "C")) "being"   ($#v6_altcat_1 :::"strict"::: )    ($#l2_altcat_1 :::"category":::) "st"  (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds"  (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "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 :::"{}"::: )  )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#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 "b")) "," (Set (Var "c")) "holds"  (Bool (Set (Set (Var "g"))  ($#k5_altcat_1 :::"*"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ))))  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "b")) "," (Set (Var "c")) ")" ))) "holds"  (Bool (Set F3 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "c")) ")" ))))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "b")) "," (Set (Var "c")) ")" )) & (Bool (Set (Var "h"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "c")) "," (Set (Var "d")) ")" ))) "holds"  (Bool (Set F3 "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set F3 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ) "," (Set (Var "h")) ")" )  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "f")) "," (Set F3 "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "g")) "," (Set (Var "h")) ")" ) ")" ))))
 and  
(Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) (Bool  "ex" (Set (Var "f")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "a")) ")" )) & (Bool  "("   "for" (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "g")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "holds"  (Bool (Set F3 "(" (Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "g"))))  ")" )  ")" )))
 and  
(Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) (Bool  "ex" (Set (Var "f")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "a")) ")" )) & (Bool  "("   "for" (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "g")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "b")) "," (Set (Var "a")) ")" ))) "holds"  (Bool (Set F3 "(" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "g")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "g"))))  ")" )  ")" )))
 proof 


end; scheme  :: YELLOW18:sch 5 CategoryLambdaUniq{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F3(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )    "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C1")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "holds"  (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1"))  "st" (Bool (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#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 "b")) "," (Set (Var "c")) "holds"  (Bool (Set (Set (Var "g"))  ($#k5_altcat_1 :::"*"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ))))  ")" ) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C2")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C2")) "holds"  (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C2"))  "st" (Bool (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#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 "b")) "," (Set (Var "c")) "holds"  (Bool (Set (Set (Var "g"))  ($#k5_altcat_1 :::"*"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ))))  ")" )) "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"))) "#)" )))
 proof 


end; scheme  :: YELLOW18:sch 6 CategoryQuasiLambda{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ], F2(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F3(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "ex" (Set (Var "C")) "being"   ($#v6_altcat_1 :::"strict"::: )    ($#l2_altcat_1 :::"category":::) "st"  (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "f")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))])  ")" )  ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "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 :::"{}"::: )  )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#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 "b")) "," (Set (Var "c")) "holds"  (Bool (Set (Set (Var "g"))  ($#k5_altcat_1 :::"*"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ))))  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))]) & (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "b")) "," (Set (Var "c")) ")" )) & (Bool P1[(Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "g"))])) "holds"  (Bool  "("  (Bool (Set F3 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "c")) ")" )) & (Bool P1[(Set (Var "a")) "," (Set (Var "c")) "," (Set F3 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "g")) ")" )])  ")" )))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))]) & (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "b")) "," (Set (Var "c")) ")" )) & (Bool P1[(Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "g"))]) & (Bool (Set (Var "h"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "c")) "," (Set (Var "d")) ")" )) & (Bool P1[(Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "h"))])) "holds"  (Bool (Set F3 "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set F3 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ) "," (Set (Var "h")) ")" )  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "f")) "," (Set F3 "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "g")) "," (Set (Var "h")) ")" ) ")" ))))
 and  
(Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) (Bool  "ex" (Set (Var "f")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "a")) ")" )) & (Bool P1[(Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "f"))]) & (Bool  "("   "for" (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "g")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "g"))])) "holds"  (Bool (Set F3 "(" (Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "g"))))  ")" )  ")" )))
 and  
(Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) (Bool  "ex" (Set (Var "f")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "a")) ")" )) & (Bool P1[(Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "f"))]) & (Bool  "("   "for" (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "g")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "b")) "," (Set (Var "a")) ")" )) & (Bool P1[(Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "g"))])) "holds"  (Bool (Set F3 "(" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "g")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "g"))))  ")" )  ")" )))
 proof 


end; registrationlet "f" be   ($#v1_funcop_1 :::"Function-yielding"::: )    ($#m1_hidden :::"Function":::); let "a", "b", "c" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "f"  ($#k1_multop_1 :::"."::: )   "(" "a" "," "b" "," "c" ")" ) ->   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )   ; 
end; scheme  :: YELLOW18:sch 7 SubcategoryEx{ F1() ->   ($#l2_altcat_1 :::"category":::), P1[   ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "B")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_altcat_1 :::"strict"::: )    ($#m1_altcat_2 :::"subcategory":::) "of" (Set F1 "("  ")" ) "st"  (Bool  "("  (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"))])  ")" )  ")" ) & (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 (Var "B"))  "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"))])  ")" )))  ")" )  ")" ))
 provided
(Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" ) "st" (Bool P1[(Set (Var "a"))]))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "a"))]) & (Bool P1[(Set (Var "b"))]) & (Bool P1[(Set (Var "c"))]) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#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 "b")) "," (Set (Var "c"))  "st" (Bool (Bool P2[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))]) & (Bool P2[(Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "g"))])) "holds"  (Bool P2[(Set (Var "a")) "," (Set (Var "c")) "," (Set (Set (Var "g"))  ($#k5_altcat_1 :::"*"::: )  (Set (Var "f")))]))))
 and  
(Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "a"))])) "holds"  (Bool P2[(Set (Var "a")) "," (Set (Var "a")) "," (Set   ($#k8_altcat_1 :::"idm"::: )  (Set (Var "a")))]))
 proof 


end; scheme  :: YELLOW18:sch 8 CovariantFunctorLambda{ F1() ->   ($#l2_altcat_1 :::"category":::), F2() ->   ($#l2_altcat_1 :::"category":::), F3(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F4(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "ex" (Set (Var "F")) "being"   ($#v9_functor0 :::"strict"::: )     ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_functor0 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "a")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "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 (Var "f")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" )))  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set F3 "(" (Set (Var "a")) ")" ) "is"   ($#m1_subset_1 :::"object":::) "of" (Set F2 "("  ")" )))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "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 F4 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" )  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set F2 "("  ")" ))  ($#k1_binop_1 :::"."::: )   "(" (Set F3 "(" (Set (Var "a")) ")" ) "," (Set F3 "(" (Set (Var "b")) ")" ) ")" ))))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#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 "b")) "," (Set (Var "c"))  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F2 "("  ")" )  "st" (Bool (Bool (Set (Var "a9"))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "a")) ")" )) & (Bool (Set (Var "b9"))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "b")) ")" )) & (Bool (Set (Var "c9"))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "c")) ")" ))) "holds"  (Bool  "for" (Set (Var "f9")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a9")) "," (Set (Var "b9"))  (Bool  "for" (Set (Var "g9")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b9")) "," (Set (Var "c9"))  "st" (Bool (Bool (Set (Var "f9"))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" )) & (Bool (Set (Var "g9"))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "g")) ")" ))) "holds"  (Bool (Set F4 "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set  "(" (Set (Var "g"))  ($#k5_altcat_1 :::"*"::: )  (Set (Var "f")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "g9"))  ($#k5_altcat_1 :::"*"::: )  (Set (Var "f9"))))))))))
 and  
(Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "a9")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F2 "("  ")" )  "st" (Bool (Bool (Set (Var "a9"))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "a")) ")" ))) "holds"  (Bool (Set F4 "(" (Set (Var "a")) "," (Set (Var "a")) "," (Set  "("  ($#k8_altcat_1 :::"idm"::: )  (Set (Var "a")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_altcat_1 :::"idm"::: )  (Set (Var "a9"))))))
 proof 


end; 
theorem :: YELLOW18:1 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l2_altcat_1 :::"category":::)  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set (Var "A")) "," (Set (Var "B"))  "st" (Bool (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_functor0 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k3_functor0 :::"."::: )  (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 "F"))  ($#k6_functor0 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k6_functor0 :::"."::: )  (Set (Var "f")))))  ")" )) "holds"  (Bool (Set   ($#g2_functor0 :::"FunctorStr"::: )  "(#"  (Set  "the"  ($#u1_functor0 :::"ObjectMap"::: )  "of" (Set (Var "F"))) "," (Set  "the"  ($#u2_functor0 :::"MorphMap"::: )  "of" (Set (Var "F"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g2_functor0 :::"FunctorStr"::: )  "(#"  (Set  "the"  ($#u1_functor0 :::"ObjectMap"::: )  "of" (Set (Var "G"))) "," (Set  "the"  ($#u2_functor0 :::"MorphMap"::: )  "of" (Set (Var "G"))) "#)" )))) ; 
 scheme  :: YELLOW18:sch 9 ContravariantFunctorLambda{ F1() ->   ($#l2_altcat_1 :::"category":::), F2() ->   ($#l2_altcat_1 :::"category":::), F3(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F4(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "ex" (Set (Var "F")) "being"   ($#v9_functor0 :::"strict"::: )     ($#v16_functor0 :::"contravariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_functor0 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "a")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "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 (Var "f")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" )))  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set F3 "(" (Set (Var "a")) ")" ) "is"   ($#m1_subset_1 :::"object":::) "of" (Set F2 "("  ")" )))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "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 F4 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" )  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set F2 "("  ")" ))  ($#k1_binop_1 :::"."::: )   "(" (Set F3 "(" (Set (Var "b")) ")" ) "," (Set F3 "(" (Set (Var "a")) ")" ) ")" ))))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#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 "b")) "," (Set (Var "c"))  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F2 "("  ")" )  "st" (Bool (Bool (Set (Var "a9"))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "a")) ")" )) & (Bool (Set (Var "b9"))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "b")) ")" )) & (Bool (Set (Var "c9"))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "c")) ")" ))) "holds"  (Bool  "for" (Set (Var "f9")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b9")) "," (Set (Var "a9"))  (Bool  "for" (Set (Var "g9")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "c9")) "," (Set (Var "b9"))  "st" (Bool (Bool (Set (Var "f9"))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" )) & (Bool (Set (Var "g9"))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "g")) ")" ))) "holds"  (Bool (Set F4 "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set  "(" (Set (Var "g"))  ($#k5_altcat_1 :::"*"::: )  (Set (Var "f")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f9"))  ($#k5_altcat_1 :::"*"::: )  (Set (Var "g9"))))))))))
 and  
(Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "a9")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F2 "("  ")" )  "st" (Bool (Bool (Set (Var "a9"))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "a")) ")" ))) "holds"  (Bool (Set F4 "(" (Set (Var "a")) "," (Set (Var "a")) "," (Set  "("  ($#k8_altcat_1 :::"idm"::: )  (Set (Var "a")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_altcat_1 :::"idm"::: )  (Set (Var "a9"))))))
 proof 


end; 
theorem :: YELLOW18:2 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l2_altcat_1 :::"category":::)  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#v16_functor0 :::"contravariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set (Var "A")) "," (Set (Var "B"))  "st" (Bool (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_functor0 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k3_functor0 :::"."::: )  (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 "F"))  ($#k8_functor0 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k8_functor0 :::"."::: )  (Set (Var "f")))))  ")" )) "holds"  (Bool (Set   ($#g2_functor0 :::"FunctorStr"::: )  "(#"  (Set  "the"  ($#u1_functor0 :::"ObjectMap"::: )  "of" (Set (Var "F"))) "," (Set  "the"  ($#u2_functor0 :::"MorphMap"::: )  "of" (Set (Var "F"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g2_functor0 :::"FunctorStr"::: )  "(#"  (Set  "the"  ($#u1_functor0 :::"ObjectMap"::: )  "of" (Set (Var "G"))) "," (Set  "the"  ($#u2_functor0 :::"MorphMap"::: )  "of" (Set (Var "G"))) "#)" )))) ; 
 begin  definitionlet "A", "B", "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "C")); :: original: :::"one-to-one"::: redefine attr "f" is  :::"one-to-one":::  means :: YELLOW18:def 1 (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "A"  (Bool  "for" (Set (Var "b1")) "," (Set (Var "b2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "B"  "st" (Bool (Bool (Set "f"  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "a1")) "," (Set (Var "b1")) ")" )  ($#r1_hidden :::"="::: )  (Set "f"  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "a2")) "," (Set (Var "b2")) ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "a1"))  ($#r1_hidden :::"="::: )  (Set (Var "a2"))) & (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Var "b2")))  ")" ))); end; 







:: deftheorem    defines :::"one-to-one"::: YELLOW18:def 1 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) "iff" (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "b1")) "," (Set (Var "b2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "B"))  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "a1")) "," (Set (Var "b1")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "a2")) "," (Set (Var "b2")) ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "a1"))  ($#r1_hidden :::"="::: )  (Set (Var "a2"))) & (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Var "b2")))  ")" )))  ")" ))); 
 scheme  :: YELLOW18:sch 10 CoBijectiveSch{ F1() ->   ($#l2_altcat_1 :::"category":::), F2() ->   ($#l2_altcat_1 :::"category":::), F3() ->   ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set F1 "("  ")" ) "," (Set F2 "("  ")" ), F4(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F5(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool (Set F3 "("  ")" ) "is"   ($#v21_functor0 :::"bijective"::: )  )
 provided
(Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set (Set F3 "("  ")" )  ($#k3_functor0 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "a")) ")" )))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "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 F3 "("  ")" )  ($#k6_functor0 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" ))))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set F4 "(" (Set (Var "a")) ")" )  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "b")) ")" ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "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 F5 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "g")) ")" ))) "holds"  (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F2 "("  ")" )  "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 F1 "("  ")" )(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 F4 "(" (Set (Var "c")) ")" )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set F4 "(" (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 F5 "(" (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "g")) ")" ))  ")" )))))
 proof 


end; scheme  :: YELLOW18:sch 11 CatIsomorphism{ F1() ->   ($#l2_altcat_1 :::"category":::), F2() ->   ($#l2_altcat_1 :::"category":::), F3(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F4(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool (Set F1 "("  ")" ) "," (Set F2 "("  ")" )  ($#r1_functor0 :::"are_isomorphic"::: )  )
 provided
(Bool  "ex" (Set (Var "F")) "being"   ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_functor0 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "a")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "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 (Var "f")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" )))  ")" )  ")" ))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set F3 "(" (Set (Var "a")) ")" )  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "b")) ")" ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "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 F4 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "g")) ")" ))) "holds"  (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F2 "("  ")" )  "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 F1 "("  ")" )(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 F3 "(" (Set (Var "c")) ")" )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set F3 "(" (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 F4 "(" (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "g")) ")" ))  ")" )))))
 proof 


end; scheme  :: YELLOW18:sch 12 ContraBijectiveSch{ F1() ->   ($#l2_altcat_1 :::"category":::), F2() ->   ($#l2_altcat_1 :::"category":::), F3() ->   ($#v16_functor0 :::"contravariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set F1 "("  ")" ) "," (Set F2 "("  ")" ), F4(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F5(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool (Set F3 "("  ")" ) "is"   ($#v21_functor0 :::"bijective"::: )  )
 provided
(Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set (Set F3 "("  ")" )  ($#k3_functor0 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "a")) ")" )))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "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 F3 "("  ")" )  ($#k8_functor0 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" ))))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set F4 "(" (Set (Var "a")) ")" )  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "b")) ")" ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "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 F5 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "g")) ")" ))) "holds"  (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F2 "("  ")" )  "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 F1 "("  ")" )(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 F4 "(" (Set (Var "c")) ")" )) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set F4 "(" (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 F5 "(" (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "g")) ")" ))  ")" )))))
 proof 


end; scheme  :: YELLOW18:sch 13 CatAntiIsomorphism{ F1() ->   ($#l2_altcat_1 :::"category":::), F2() ->   ($#l2_altcat_1 :::"category":::), F3(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F4(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool (Set F1 "("  ")" ) "," (Set F2 "("  ")" )  ($#r2_functor0 :::"are_anti-isomorphic"::: )  )
 provided
(Bool  "ex" (Set (Var "F")) "being"   ($#v16_functor0 :::"contravariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_functor0 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "a")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "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 (Var "f")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" )))  ")" )  ")" ))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set F3 "(" (Set (Var "a")) ")" )  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "b")) ")" ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "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 F4 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "g")) ")" ))) "holds"  (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F2 "("  ")" )  "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 F1 "("  ")" )(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 F3 "(" (Set (Var "c")) ")" )) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set F3 "(" (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 F4 "(" (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "g")) ")" ))  ")" )))))
 proof 


end; definitionlet "A", "B" be   ($#l2_altcat_1 :::"category":::); pred "A" "," "B" :::"are_equivalent":::  means :: YELLOW18:def 2 (Bool  "ex" (Set (Var "F")) "being"   ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" "A" "," "B"(Bool  "ex" (Set (Var "G")) "being"   ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" "B" "," "A" "st"  (Bool  "("  (Bool (Set (Set (Var "G"))  ($#k1_functor3 :::"*"::: )  (Set (Var "F"))) "," (Set   ($#k12_functor0 :::"id"::: )  "A")  ($#r1_functor3 :::"are_naturally_equivalent"::: )  ) & (Bool (Set (Set (Var "F"))  ($#k1_functor3 :::"*"::: )  (Set (Var "G"))) "," (Set   ($#k12_functor0 :::"id"::: )  "B")  ($#r1_functor3 :::"are_naturally_equivalent"::: )  )  ")" ))); reflexivity  
(Bool  "for" (Set (Var "A")) "being"   ($#l2_altcat_1 :::"category":::) (Bool  "ex" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set (Var "A")) "," (Set (Var "A")) "st"  (Bool  "("  (Bool (Set (Set (Var "G"))  ($#k1_functor3 :::"*"::: )  (Set (Var "F"))) "," (Set   ($#k12_functor0 :::"id"::: )  (Set (Var "A")))  ($#r1_functor3 :::"are_naturally_equivalent"::: )  ) & (Bool (Set (Set (Var "F"))  ($#k1_functor3 :::"*"::: )  (Set (Var "G"))) "," (Set   ($#k12_functor0 :::"id"::: )  (Set (Var "A")))  ($#r1_functor3 :::"are_naturally_equivalent"::: )  )  ")" )))
 ; symmetry  
(Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool  "ex" (Set (Var "F")) "being"   ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set (Var "A")) "," (Set (Var "B"))(Bool  "ex" (Set (Var "G")) "being"   ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set (Var "B")) "," (Set (Var "A")) "st"  (Bool  "("  (Bool (Set (Set (Var "G"))  ($#k1_functor3 :::"*"::: )  (Set (Var "F"))) "," (Set   ($#k12_functor0 :::"id"::: )  (Set (Var "A")))  ($#r1_functor3 :::"are_naturally_equivalent"::: )  ) & (Bool (Set (Set (Var "F"))  ($#k1_functor3 :::"*"::: )  (Set (Var "G"))) "," (Set   ($#k12_functor0 :::"id"::: )  (Set (Var "B")))  ($#r1_functor3 :::"are_naturally_equivalent"::: )  )  ")" )))) "holds"  (Bool  "ex" (Set (Var "F")) "being"   ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set (Var "B")) "," (Set (Var "A"))(Bool  "ex" (Set (Var "G")) "being"   ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set (Var "A")) "," (Set (Var "B")) "st"  (Bool  "("  (Bool (Set (Set (Var "G"))  ($#k1_functor3 :::"*"::: )  (Set (Var "F"))) "," (Set   ($#k12_functor0 :::"id"::: )  (Set (Var "B")))  ($#r1_functor3 :::"are_naturally_equivalent"::: )  ) & (Bool (Set (Set (Var "F"))  ($#k1_functor3 :::"*"::: )  (Set (Var "G"))) "," (Set   ($#k12_functor0 :::"id"::: )  (Set (Var "A")))  ($#r1_functor3 :::"are_naturally_equivalent"::: )  )  ")" ))))
 ; end; 





:: deftheorem    defines :::"are_equivalent"::: YELLOW18:def 2 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l2_altcat_1 :::"category":::) "holds"   (Bool  "("  (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r1_yellow18 :::"are_equivalent"::: )  ) "iff" (Bool  "ex" (Set (Var "F")) "being"   ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set (Var "A")) "," (Set (Var "B"))(Bool  "ex" (Set (Var "G")) "being"   ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set (Var "B")) "," (Set (Var "A")) "st"  (Bool  "("  (Bool (Set (Set (Var "G"))  ($#k1_functor3 :::"*"::: )  (Set (Var "F"))) "," (Set   ($#k12_functor0 :::"id"::: )  (Set (Var "A")))  ($#r1_functor3 :::"are_naturally_equivalent"::: )  ) & (Bool (Set (Set (Var "F"))  ($#k1_functor3 :::"*"::: )  (Set (Var "G"))) "," (Set   ($#k12_functor0 :::"id"::: )  (Set (Var "B")))  ($#r1_functor3 :::"are_naturally_equivalent"::: )  )  ")" )))  ")" )); 
 
theorem :: YELLOW18:3 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_altcat_2 :::"reflexive"::: )     ($#l1_altcat_1 :::"AltGraph"::: )    (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"   ($#v8_functor0 :::"feasible"::: )     ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "A")) "," (Set (Var "B"))  (Bool  "for" (Set (Var "G1")) "," (Set (Var "G2")) "being"    ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "B")) "," (Set (Var "C"))  "st" (Bool (Bool (Set   ($#g2_functor0 :::"FunctorStr"::: )  "(#"  (Set  "the"  ($#u1_functor0 :::"ObjectMap"::: )  "of" (Set (Var "F1"))) "," (Set  "the"  ($#u2_functor0 :::"MorphMap"::: )  "of" (Set (Var "F1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g2_functor0 :::"FunctorStr"::: )  "(#"  (Set  "the"  ($#u1_functor0 :::"ObjectMap"::: )  "of" (Set (Var "F2"))) "," (Set  "the"  ($#u2_functor0 :::"MorphMap"::: )  "of" (Set (Var "F2"))) "#)" )) & (Bool (Set   ($#g2_functor0 :::"FunctorStr"::: )  "(#"  (Set  "the"  ($#u1_functor0 :::"ObjectMap"::: )  "of" (Set (Var "G1"))) "," (Set  "the"  ($#u2_functor0 :::"MorphMap"::: )  "of" (Set (Var "G1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g2_functor0 :::"FunctorStr"::: )  "(#"  (Set  "the"  ($#u1_functor0 :::"ObjectMap"::: )  "of" (Set (Var "G2"))) "," (Set  "the"  ($#u2_functor0 :::"MorphMap"::: )  "of" (Set (Var "G2"))) "#)" ))) "holds"  (Bool (Set (Set (Var "G1"))  ($#k13_functor0 :::"*"::: )  (Set (Var "F1")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G2"))  ($#k13_functor0 :::"*"::: )  (Set (Var "F2"))))))) ; 
 
theorem :: YELLOW18:4 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r1_yellow18 :::"are_equivalent"::: )  ) & (Bool (Set (Var "B")) "," (Set (Var "C"))  ($#r1_yellow18 :::"are_equivalent"::: )  )) "holds"  (Bool (Set (Var "A")) "," (Set (Var "C"))  ($#r1_yellow18 :::"are_equivalent"::: )  )) ; 
 
theorem :: YELLOW18:5 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r1_functor0 :::"are_isomorphic"::: )  )) "holds"  (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r1_yellow18 :::"are_equivalent"::: )  )) ; 
 scheme  :: YELLOW18:sch 14 NatTransLambda{ F1() ->   ($#l2_altcat_1 :::"category":::), F2() ->   ($#l2_altcat_1 :::"category":::), F3() ->   ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set F1 "("  ")" ) "," (Set F2 "("  ")" ), F4() ->   ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set F1 "("  ")" ) "," (Set F2 "("  ")" ), F5(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "ex" (Set (Var "t")) "being"    ($#m2_functor2 :::"natural_transformation"::: )   "of" (Set F3 "("  ")" ) "," (Set F4 "("  ")" ) "st"  (Bool  "("  (Bool (Set F3 "("  ")" )  ($#r2_functor2 :::"is_naturally_transformable_to"::: )  (Set F4 "("  ")" )) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set (Set (Var "t"))  ($#k2_functor2 :::"!"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "a")) ")" ))  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set F5 "(" (Set (Var "a")) ")" )  ($#r2_hidden :::"in"::: )  (Set  ($#k1_altcat_1 :::"<^"::: ) (Set  "(" (Set F3 "("  ")" )  ($#k3_functor0 :::"."::: )  (Set (Var "a")) ")" ) "," (Set  "(" (Set F4 "("  ")" )  ($#k3_functor0 :::"."::: )  (Set (Var "a")) ")" ) ($#k1_altcat_1 :::"^>"::: ) )))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "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  "for" (Set (Var "g1")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set  "(" (Set F3 "("  ")" )  ($#k3_functor0 :::"."::: )  (Set (Var "a")) ")" ) "," (Set  "(" (Set F4 "("  ")" )  ($#k3_functor0 :::"."::: )  (Set (Var "a")) ")" )  "st" (Bool (Bool (Set (Var "g1"))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "a")) ")" ))) "holds"  (Bool  "for" (Set (Var "g2")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set  "(" (Set F3 "("  ")" )  ($#k3_functor0 :::"."::: )  (Set (Var "b")) ")" ) "," (Set  "(" (Set F4 "("  ")" )  ($#k3_functor0 :::"."::: )  (Set (Var "b")) ")" )  "st" (Bool (Bool (Set (Var "g2"))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "b")) ")" ))) "holds"  (Bool (Set (Set (Var "g2"))  ($#k5_altcat_1 :::"*"::: )  (Set  "(" (Set F3 "("  ")" )  ($#k6_functor0 :::"."::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set F4 "("  ")" )  ($#k6_functor0 :::"."::: )  (Set (Var "f")) ")" )  ($#k5_altcat_1 :::"*"::: )  (Set (Var "g1"))))))))
 proof 


end; scheme  :: YELLOW18:sch 15 NatEquivalenceLambda{ F1() ->   ($#l2_altcat_1 :::"category":::), F2() ->   ($#l2_altcat_1 :::"category":::), F3() ->   ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set F1 "("  ")" ) "," (Set F2 "("  ")" ), F4() ->   ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set F1 "("  ")" ) "," (Set F2 "("  ")" ), F5(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "ex" (Set (Var "t")) "being"    ($#m1_functor3 :::"natural_equivalence"::: )   "of" (Set F3 "("  ")" ) "," (Set F4 "("  ")" ) "st"  (Bool  "("  (Bool (Set F3 "("  ")" ) "," (Set F4 "("  ")" )  ($#r1_functor3 :::"are_naturally_equivalent"::: )  ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set (Set (Var "t"))  ($#k2_functor2 :::"!"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "a")) ")" ))  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" ) "holds"   (Bool  "("  (Bool (Set F5 "(" (Set (Var "a")) ")" )  ($#r2_hidden :::"in"::: )  (Set  ($#k1_altcat_1 :::"<^"::: ) (Set  "(" (Set F3 "("  ")" )  ($#k3_functor0 :::"."::: )  (Set (Var "a")) ")" ) "," (Set  "(" (Set F4 "("  ")" )  ($#k3_functor0 :::"."::: )  (Set (Var "a")) ")" ) ($#k1_altcat_1 :::"^>"::: ) )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set  "(" (Set F4 "("  ")" )  ($#k3_functor0 :::"."::: )  (Set (Var "a")) ")" ) "," (Set  "(" (Set F3 "("  ")" )  ($#k3_functor0 :::"."::: )  (Set (Var "a")) ")" ) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "("   "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set  "(" (Set F3 "("  ")" )  ($#k3_functor0 :::"."::: )  (Set (Var "a")) ")" ) "," (Set  "(" (Set F4 "("  ")" )  ($#k3_functor0 :::"."::: )  (Set (Var "a")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "a")) ")" ))) "holds"  (Bool (Set (Var "f")) "is"   ($#v3_altcat_3 :::"iso"::: )  )  ")" )  ")" ))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "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  "for" (Set (Var "g1")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set  "(" (Set F3 "("  ")" )  ($#k3_functor0 :::"."::: )  (Set (Var "a")) ")" ) "," (Set  "(" (Set F4 "("  ")" )  ($#k3_functor0 :::"."::: )  (Set (Var "a")) ")" )  "st" (Bool (Bool (Set (Var "g1"))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "a")) ")" ))) "holds"  (Bool  "for" (Set (Var "g2")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set  "(" (Set F3 "("  ")" )  ($#k3_functor0 :::"."::: )  (Set (Var "b")) ")" ) "," (Set  "(" (Set F4 "("  ")" )  ($#k3_functor0 :::"."::: )  (Set (Var "b")) ")" )  "st" (Bool (Bool (Set (Var "g2"))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "b")) ")" ))) "holds"  (Bool (Set (Set (Var "g2"))  ($#k5_altcat_1 :::"*"::: )  (Set  "(" (Set F3 "("  ")" )  ($#k6_functor0 :::"."::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set F4 "("  ")" )  ($#k6_functor0 :::"."::: )  (Set (Var "f")) ")" )  ($#k5_altcat_1 :::"*"::: )  (Set (Var "g1"))))))))
 proof 


end; begin  definitionlet "C1", "C2" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_altcat_1 :::"AltCatStr"::: )  ; pred "C1" "," "C2" :::"are_opposite":::  means :: YELLOW18:def 3 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "C2")  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "C1")) & (Bool (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" "C2")  ($#r1_hidden :::"="::: )  (Set   ($#k2_funct_4 :::"~"::: )  (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" "C1"))) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"object":::) "of" "C1"  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being"   ($#m1_subset_1 :::"object":::) "of" "C2"  "st" (Bool (Bool (Set (Var "a9"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "b9"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "c9"))  ($#r1_hidden :::"="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Set  "the"  ($#u2_altcat_1 :::"Comp"::: )  "of" "C2")  ($#k4_altcat_1 :::"."::: )   "(" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_functor0 :::"~"::: )  (Set  "(" (Set  "the"  ($#u2_altcat_1 :::"Comp"::: )  "of" "C1")  ($#k4_altcat_1 :::"."::: )   "(" (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) ")"  ")" ))))  ")" )  ")" ); symmetry  
(Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_altcat_1 :::"AltCatStr"::: )    "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C2")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C1")))) & (Bool (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set (Var "C2")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_funct_4 :::"~"::: )  (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set (Var "C1"))))) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1"))  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C2"))  "st" (Bool (Bool (Set (Var "a9"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "b9"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "c9"))  ($#r1_hidden :::"="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Set  "the"  ($#u2_altcat_1 :::"Comp"::: )  "of" (Set (Var "C2")))  ($#k4_altcat_1 :::"."::: )   "(" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_functor0 :::"~"::: )  (Set  "(" (Set  "the"  ($#u2_altcat_1 :::"Comp"::: )  "of" (Set (Var "C1")))  ($#k4_altcat_1 :::"."::: )   "(" (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) ")"  ")" ))))  ")" )) "holds"  (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C1")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C2")))) & (Bool (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set (Var "C1")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_funct_4 :::"~"::: )  (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set (Var "C2"))))) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C2"))  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1"))  "st" (Bool (Bool (Set (Var "a9"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "b9"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "c9"))  ($#r1_hidden :::"="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Set  "the"  ($#u2_altcat_1 :::"Comp"::: )  "of" (Set (Var "C1")))  ($#k4_altcat_1 :::"."::: )   "(" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_functor0 :::"~"::: )  (Set  "(" (Set  "the"  ($#u2_altcat_1 :::"Comp"::: )  "of" (Set (Var "C2")))  ($#k4_altcat_1 :::"."::: )   "(" (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) ")"  ")" ))))  ")" )  ")" ))
 ; end; 





:: deftheorem    defines :::"are_opposite"::: YELLOW18:def 3 :  (Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_altcat_1 :::"AltCatStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "C1")) "," (Set (Var "C2"))  ($#r2_yellow18 :::"are_opposite"::: )  ) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C2")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C1")))) & (Bool (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set (Var "C2")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_funct_4 :::"~"::: )  (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set (Var "C1"))))) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1"))  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C2"))  "st" (Bool (Bool (Set (Var "a9"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "b9"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "c9"))  ($#r1_hidden :::"="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Set  "the"  ($#u2_altcat_1 :::"Comp"::: )  "of" (Set (Var "C2")))  ($#k4_altcat_1 :::"."::: )   "(" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_functor0 :::"~"::: )  (Set  "(" (Set  "the"  ($#u2_altcat_1 :::"Comp"::: )  "of" (Set (Var "C1")))  ($#k4_altcat_1 :::"."::: )   "(" (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) ")"  ")" ))))  ")" )  ")" )  ")" )); 
 
theorem :: YELLOW18:6 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_altcat_1 :::"AltCatStr"::: )    "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_yellow18 :::"are_opposite"::: )  )) "holds"  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Var "a")) "is"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "B"))))) ; 
 
theorem :: YELLOW18:7 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_altcat_1 :::"AltCatStr"::: )    "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_yellow18 :::"are_opposite"::: )  )) "holds"  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "B"))  "st" (Bool (Bool (Set (Var "a9"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "b9"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "holds"  (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b9")) "," (Set (Var "a9")) ($#k1_altcat_1 :::"^>"::: ) ))))) ; 
 
theorem :: YELLOW18:8 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_altcat_1 :::"AltCatStr"::: )    "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_yellow18 :::"are_opposite"::: )  )) "holds"  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "B"))  "st" (Bool (Bool (Set (Var "a9"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "b9"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds"  (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b9")) "," (Set (Var "a9"))))))) ; 
 
theorem :: YELLOW18:9 (Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "C1")) "," (Set (Var "C2"))  ($#r2_yellow18 :::"are_opposite"::: )  ) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C2")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C1")))) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1"))  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C2"))  "st" (Bool (Bool (Set (Var "a9"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "b9"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "c9"))  ($#r1_hidden :::"="::: )  (Set (Var "c")))) "holds"  (Bool  "("  (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b9")) "," (Set (Var "a9")) ($#k1_altcat_1 :::"^>"::: ) )) &  "("  (Bool (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (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 "b")) "," (Set (Var "c"))  (Bool  "for" (Set (Var "f9")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b9")) "," (Set (Var "a9"))  (Bool  "for" (Set (Var "g9")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "c9")) "," (Set (Var "b9"))  "st" (Bool (Bool (Set (Var "f9"))  ($#r1_hidden :::"="::: )  (Set (Var "f"))) & (Bool (Set (Var "g9"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) "holds"  (Bool (Set (Set (Var "f9"))  ($#k5_altcat_1 :::"*"::: )  (Set (Var "g9")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k5_altcat_1 :::"*"::: )  (Set (Var "f"))))))))  ")"   ")" ))  ")" )  ")" )  ")" )) ; 
 
theorem :: YELLOW18:10 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_yellow18 :::"are_opposite"::: )  )) "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"))  "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"))))))) ; 
 
theorem :: YELLOW18: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"::: )    "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_yellow18 :::"are_opposite"::: )  ) & (Bool (Set (Var "A")) "is"   ($#v11_altcat_1 :::"associative"::: )  )) "holds"  (Bool (Set (Var "B")) "is"   ($#v11_altcat_1 :::"associative"::: )  )) ; 
 
theorem :: YELLOW18:12 (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"::: )    "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_yellow18 :::"are_opposite"::: )  ) & (Bool (Set (Var "A")) "is"   ($#v12_altcat_1 :::"with_units"::: )  )) "holds"  (Bool (Set (Var "B")) "is"   ($#v12_altcat_1 :::"with_units"::: )  )) ; 
 
theorem :: YELLOW18:13 (Bool  "for" (Set (Var "C")) "," (Set (Var "C1")) "," (Set (Var "C2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_altcat_1 :::"AltCatStr"::: )    "st" (Bool (Bool (Set (Var "C")) "," (Set (Var "C1"))  ($#r2_yellow18 :::"are_opposite"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "C")) "," (Set (Var "C2"))  ($#r2_yellow18 :::"are_opposite"::: )  ) "iff" (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"))) "#)" ))  ")" )) ; 
 definitionlet "C" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )  ; func "C" :::"opp":::  ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#v6_altcat_1 :::"strict"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )   means :: YELLOW18:def 4 (Bool "C" "," it  ($#r2_yellow18 :::"are_opposite"::: )  ); end; 





:: deftheorem    defines :::"opp"::: YELLOW18:def 4 :  (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 "b2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#v6_altcat_1 :::"strict"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "C"))  ($#k1_yellow18 :::"opp"::: )  )) "iff" (Bool (Set (Var "C")) "," (Set (Var "b2"))  ($#r2_yellow18 :::"are_opposite"::: )  )  ")" ))); 
 registrationlet "C" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#v11_altcat_1 :::"associative"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )  ; 
cluster (Set "C"  ($#k1_yellow18 :::"opp"::: )  ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#v6_altcat_1 :::"strict"::: )     ($#v11_altcat_1 :::"associative"::: )   ; 
end; 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 (Set "C"  ($#k1_yellow18 :::"opp"::: )  ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#v6_altcat_1 :::"strict"::: )     ($#v12_altcat_1 :::"with_units"::: )   ; 
end; definitionlet "A", "B" be   ($#l2_altcat_1 :::"category":::); assume 
(Bool (Set (Const "A")) "," (Set (Const "B"))  ($#r2_yellow18 :::"are_opposite"::: )  )
 ; func  :::"dualizing-func":::  "(" "A" "," "B" ")"  ->   ($#v9_functor0 :::"strict"::: )     ($#v16_functor0 :::"contravariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" "A" "," "B" means :: YELLOW18:def 5 (Bool  "("  (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" "A" "holds"  (Bool (Set it  ($#k3_functor0 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" "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 it  ($#k8_functor0 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "f"))))  ")" )  ")" ); end; 







:: deftheorem    defines :::"dualizing-func"::: YELLOW18:def 5 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_yellow18 :::"are_opposite"::: )  )) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#v9_functor0 :::"strict"::: )     ($#v16_functor0 :::"contravariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set (Var "A")) "," (Set (Var "B")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_yellow18 :::"dualizing-func"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set (Var "b3"))  ($#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 "b3"))  ($#k8_functor0 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "f"))))  ")" )  ")" )  ")" ))); 
 
theorem :: YELLOW18:14 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_yellow18 :::"are_opposite"::: )  )) "holds"  (Bool (Set (Set  "("  ($#k2_yellow18 :::"dualizing-func"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")"  ")" )  ($#k2_functor3 :::"*"::: )  (Set  "("  ($#k2_yellow18 :::"dualizing-func"::: )   "(" (Set (Var "B")) "," (Set (Var "A")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k12_functor0 :::"id"::: )  (Set (Var "B"))))) ; 
 
theorem :: YELLOW18:15 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_yellow18 :::"are_opposite"::: )  )) "holds"  (Bool (Set   ($#k2_yellow18 :::"dualizing-func"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) "is"   ($#v21_functor0 :::"bijective"::: )  )) ; 
 registrationlet "A" be   ($#l2_altcat_1 :::"category":::); 
cluster (Set   ($#k2_yellow18 :::"dualizing-func"::: )   "(" "A" "," (Set  "(" "A"  ($#k1_yellow18 :::"opp"::: )  ")" ) ")" ) ->   ($#v9_functor0 :::"strict"::: )     ($#v16_functor0 :::"contravariant"::: )     ($#v21_functor0 :::"bijective"::: )   ; 

cluster (Set   ($#k2_yellow18 :::"dualizing-func"::: )   "(" (Set  "(" "A"  ($#k1_yellow18 :::"opp"::: )  ")" ) "," "A" ")" ) ->   ($#v9_functor0 :::"strict"::: )     ($#v16_functor0 :::"contravariant"::: )     ($#v21_functor0 :::"bijective"::: )   ; 
end; 
theorem :: YELLOW18:16 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_yellow18 :::"are_opposite"::: )  )) "holds"  (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_functor0 :::"are_anti-isomorphic"::: )  )) ; 
 
theorem :: YELLOW18:17 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_yellow18 :::"are_opposite"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "A")) "," (Set (Var "C"))  ($#r1_functor0 :::"are_isomorphic"::: )  ) "iff" (Bool (Set (Var "B")) "," (Set (Var "C"))  ($#r2_functor0 :::"are_anti-isomorphic"::: )  )  ")" )) ; 
 
theorem :: YELLOW18:18 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_yellow18 :::"are_opposite"::: )  ) & (Bool (Set (Var "C")) "," (Set (Var "D"))  ($#r2_yellow18 :::"are_opposite"::: )  ) & (Bool (Set (Var "A")) "," (Set (Var "C"))  ($#r1_functor0 :::"are_isomorphic"::: )  )) "holds"  (Bool (Set (Var "B")) "," (Set (Var "D"))  ($#r1_functor0 :::"are_isomorphic"::: )  )) ; 
 
theorem :: YELLOW18:19 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_yellow18 :::"are_opposite"::: )  ) & (Bool (Set (Var "C")) "," (Set (Var "D"))  ($#r2_yellow18 :::"are_opposite"::: )  ) & (Bool (Set (Var "A")) "," (Set (Var "C"))  ($#r2_functor0 :::"are_anti-isomorphic"::: )  )) "holds"  (Bool (Set (Var "B")) "," (Set (Var "D"))  ($#r2_functor0 :::"are_anti-isomorphic"::: )  )) ; 
 
theorem :: YELLOW18:20 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_yellow18 :::"are_opposite"::: )  )) "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 :::"{}"::: )  )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "B"))  "st" (Bool (Bool (Set (Var "a9"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "b9"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b"))  (Bool  "for" (Set (Var "f9")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b9")) "," (Set (Var "a9"))  "st" (Bool (Bool (Set (Var "f9"))  ($#r1_hidden :::"="::: )  (Set (Var "f")))) "holds"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_altcat_3 :::"retraction"::: )  ) "iff" (Bool (Set (Var "f9")) "is"   ($#v2_altcat_3 :::"coretraction"::: )  )  ")" )))))) ; 
 
theorem :: YELLOW18:21 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_yellow18 :::"are_opposite"::: )  )) "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 :::"{}"::: )  )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "B"))  "st" (Bool (Bool (Set (Var "a9"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "b9"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b"))  (Bool  "for" (Set (Var "f9")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b9")) "," (Set (Var "a9"))  "st" (Bool (Bool (Set (Var "f9"))  ($#r1_hidden :::"="::: )  (Set (Var "f")))) "holds"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_altcat_3 :::"coretraction"::: )  ) "iff" (Bool (Set (Var "f9")) "is"   ($#v1_altcat_3 :::"retraction"::: )  )  ")" )))))) ; 
 
theorem :: YELLOW18:22 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_yellow18 :::"are_opposite"::: )  )) "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 :::"{}"::: )  )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "B"))  "st" (Bool (Bool (Set (Var "a9"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "b9"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b"))  (Bool  "for" (Set (Var "f9")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b9")) "," (Set (Var "a9"))  "st" (Bool (Bool (Set (Var "f9"))  ($#r1_hidden :::"="::: )  (Set (Var "f"))) & (Bool (Set (Var "f")) "is"   ($#v1_altcat_3 :::"retraction"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_altcat_3 :::"coretraction"::: )  )) "holds"  (Bool (Set (Set (Var "f9"))  ($#k1_altcat_3 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_altcat_3 :::"""::: )  ))))))) ; 
 
theorem :: YELLOW18:23 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_yellow18 :::"are_opposite"::: )  )) "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 :::"{}"::: )  )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "B"))  "st" (Bool (Bool (Set (Var "a9"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "b9"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b"))  (Bool  "for" (Set (Var "f9")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b9")) "," (Set (Var "a9"))  "st" (Bool (Bool (Set (Var "f9"))  ($#r1_hidden :::"="::: )  (Set (Var "f")))) "holds"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_altcat_3 :::"iso"::: )  ) "iff" (Bool (Set (Var "f9")) "is"   ($#v3_altcat_3 :::"iso"::: )  )  ")" )))))) ; 
 
theorem :: YELLOW18:24 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_yellow18 :::"are_opposite"::: )  ) & (Bool (Set (Var "C")) "," (Set (Var "D"))  ($#r2_yellow18 :::"are_opposite"::: )  )) "holds"  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set (Var "B")) "," (Set (Var "C"))  "st" (Bool (Bool (Set (Var "F")) "," (Set (Var "G"))  ($#r1_functor3 :::"are_naturally_equivalent"::: )  )) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k2_yellow18 :::"dualizing-func"::: )   "(" (Set (Var "C")) "," (Set (Var "D")) ")"  ")" )  ($#k3_functor3 :::"*"::: )  (Set (Var "G")) ")" )  ($#k2_functor3 :::"*"::: )  (Set  "("  ($#k2_yellow18 :::"dualizing-func"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")"  ")" )) "," (Set (Set  "(" (Set  "("  ($#k2_yellow18 :::"dualizing-func"::: )   "(" (Set (Var "C")) "," (Set (Var "D")) ")"  ")" )  ($#k3_functor3 :::"*"::: )  (Set (Var "F")) ")" )  ($#k2_functor3 :::"*"::: )  (Set  "("  ($#k2_yellow18 :::"dualizing-func"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")"  ")" ))  ($#r1_functor3 :::"are_naturally_equivalent"::: )  ))) ; 
 
theorem :: YELLOW18:25 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_yellow18 :::"are_opposite"::: )  ) & (Bool (Set (Var "C")) "," (Set (Var "D"))  ($#r2_yellow18 :::"are_opposite"::: )  ) & (Bool (Set (Var "A")) "," (Set (Var "C"))  ($#r1_yellow18 :::"are_equivalent"::: )  )) "holds"  (Bool (Set (Var "B")) "," (Set (Var "D"))  ($#r1_yellow18 :::"are_equivalent"::: )  )) ; 
 definitionlet "A", "B" be   ($#l2_altcat_1 :::"category":::); pred "A" "," "B" :::"are_dual":::  means :: YELLOW18:def 6 (Bool "A" "," (Set "B"  ($#k1_yellow18 :::"opp"::: )  )  ($#r1_yellow18 :::"are_equivalent"::: )  ); symmetry  
(Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Set (Var "B"))  ($#k1_yellow18 :::"opp"::: )  )  ($#r1_yellow18 :::"are_equivalent"::: )  )) "holds"  (Bool (Set (Var "B")) "," (Set (Set (Var "A"))  ($#k1_yellow18 :::"opp"::: )  )  ($#r1_yellow18 :::"are_equivalent"::: )  ))
 ; end; 





:: deftheorem    defines :::"are_dual"::: YELLOW18:def 6 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l2_altcat_1 :::"category":::) "holds"   (Bool  "("  (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r3_yellow18 :::"are_dual"::: )  ) "iff" (Bool (Set (Var "A")) "," (Set (Set (Var "B"))  ($#k1_yellow18 :::"opp"::: )  )  ($#r1_yellow18 :::"are_equivalent"::: )  )  ")" )); 
 
theorem :: YELLOW18:26 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_functor0 :::"are_anti-isomorphic"::: )  )) "holds"  (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r3_yellow18 :::"are_dual"::: )  )) ; 
 
theorem :: YELLOW18:27 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_yellow18 :::"are_opposite"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "A")) "," (Set (Var "C"))  ($#r1_yellow18 :::"are_equivalent"::: )  ) "iff" (Bool (Set (Var "B")) "," (Set (Var "C"))  ($#r3_yellow18 :::"are_dual"::: )  )  ")" )) ; 
 
theorem :: YELLOW18:28 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r3_yellow18 :::"are_dual"::: )  ) & (Bool (Set (Var "B")) "," (Set (Var "C"))  ($#r1_yellow18 :::"are_equivalent"::: )  )) "holds"  (Bool (Set (Var "A")) "," (Set (Var "C"))  ($#r3_yellow18 :::"are_dual"::: )  )) ; 
 
theorem :: YELLOW18:29 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r3_yellow18 :::"are_dual"::: )  ) & (Bool (Set (Var "B")) "," (Set (Var "C"))  ($#r3_yellow18 :::"are_dual"::: )  )) "holds"  (Bool (Set (Var "A")) "," (Set (Var "C"))  ($#r1_yellow18 :::"are_equivalent"::: )  )) ; 
 begin  
theorem :: YELLOW18:30 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"Function":::)) & (Bool (Set   ($#k9_xtuple_0 :::"proj1"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool (Set   ($#k10_xtuple_0 :::"proj2"::: )  (Set (Var "x")))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))  ")" )  ")" )) ; 
 definitionlet "C" be   ($#l2_altcat_1 :::"category":::); attr "C" is  :::"para-functional":::  means :: YELLOW18:def 7 (Bool  "ex" (Set (Var "F")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" "C" "st"  (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "being"   ($#m1_subset_1 :::"object":::) "of" "C" "holds"  (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a1")) ")" ) "," (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a2")) ")" ) ")" )))); end; 




:: deftheorem    defines :::"para-functional"::: YELLOW18:def 7 :  (Bool  "for" (Set (Var "C")) "being"   ($#l2_altcat_1 :::"category":::) "holds"   (Bool  "("  (Bool (Set (Var "C")) "is"   ($#v2_yellow18 :::"para-functional"::: )  ) "iff" (Bool  "ex" (Set (Var "F")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "C")) "st"  (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds"  (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a1")) ")" ) "," (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a2")) ")" ) ")" ))))  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#v8_altcat_1 :::"quasi-functional"::: )     ($#v11_altcat_1 :::"associative"::: )     ($#v12_altcat_1 :::"with_units"::: )    ->   ($#v2_yellow18 :::"para-functional"::: )    for    ($#l2_altcat_1 :::"AltCatStr"::: )  ; 
end; definitionlet "C" be   ($#l2_altcat_1 :::"category":::); let "a" be    ($#m1_hidden :::"set"::: )  ; func "C" :::"-carrier_of"::: "a" ->    ($#m1_hidden :::"set"::: )   means :: YELLOW18:def 8 (Bool  "ex" (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" "C" "st"  (Bool  "("  (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  "a") & (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"proj1"::: )  (Set  "("  ($#k8_altcat_1 :::"idm"::: )  (Set (Var "b")) ")" )))  ")" )) if (Bool "a" "is"   ($#m1_subset_1 :::"object":::) "of" "C")  otherwise (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )); end; 






:: deftheorem    defines :::"-carrier_of"::: YELLOW18:def 8 :  (Bool  "for" (Set (Var "C")) "being"   ($#l2_altcat_1 :::"category":::)  (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "a")) "is"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "C"))  ($#k3_yellow18 :::"-carrier_of"::: )  (Set (Var "a")))) "iff" (Bool  "ex" (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st"  (Bool  "("  (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"proj1"::: )  (Set  "("  ($#k8_altcat_1 :::"idm"::: )  (Set (Var "b")) ")" )))  ")" ))  ")" )  ")"  &  "("  (Bool (Bool (Set (Var "a")) "is" (Bool  "not"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C"))))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "C"))  ($#k3_yellow18 :::"-carrier_of"::: )  (Set (Var "a")))) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )  ")"   ")" )))); 
 notationlet "C" be   ($#l2_altcat_1 :::"category":::); let "a" be   ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); synonym  :::"the_carrier_of"::: "a" for "C" :::"-carrier_of"::: "a"; end; definitionlet "C" be   ($#l2_altcat_1 :::"category":::); let "a" be   ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); redefine func "C" :::"-carrier_of"::: "a" equals :: YELLOW18:def 9 (Set   ($#k9_xtuple_0 :::"proj1"::: )  (Set  "("  ($#k8_altcat_1 :::"idm"::: )  "a" ")" )); end; 






:: deftheorem    defines :::"-carrier_of"::: YELLOW18:def 9 :  (Bool  "for" (Set (Var "C")) "being"   ($#l2_altcat_1 :::"category":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds"  (Bool (Set (Set (Var "C"))  ($#k3_yellow18 :::"-carrier_of"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"proj1"::: )  (Set  "("  ($#k8_altcat_1 :::"idm"::: )  (Set (Var "a")) ")" ))))); 
 
theorem :: YELLOW18:31 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set  "("  ($#k7_altcat_1 :::"EnsCat"::: )  (Set (Var "A")) ")" ) "holds"  (Bool (Set   ($#k8_altcat_1 :::"idm"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set (Var "a")))))) ; 
 
theorem :: YELLOW18:32 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set  "("  ($#k7_altcat_1 :::"EnsCat"::: )  (Set (Var "A")) ")" ) "holds"  (Bool (Set   ($#k3_yellow18 :::"the_carrier_of"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))))) ; 
 definitionlet "C" be   ($#l2_altcat_1 :::"category":::); attr "C" is  :::"set-id-inheriting":::  means :: YELLOW18:def 10 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" "C" "holds"  (Bool (Set   ($#k8_altcat_1 :::"idm"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set  "("  ($#k3_yellow18 :::"the_carrier_of"::: )  (Set (Var "a")) ")" )))); end; 




:: deftheorem    defines :::"set-id-inheriting"::: YELLOW18:def 10 :  (Bool  "for" (Set (Var "C")) "being"   ($#l2_altcat_1 :::"category":::) "holds"   (Bool  "("  (Bool (Set (Var "C")) "is"   ($#v3_yellow18 :::"set-id-inheriting"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds"  (Bool (Set   ($#k8_altcat_1 :::"idm"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set  "("  ($#k3_yellow18 :::"the_carrier_of"::: )  (Set (Var "a")) ")" ))))  ")" )); 
 registrationlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k7_altcat_1 :::"EnsCat"::: )  "A") ->   ($#v3_yellow18 :::"set-id-inheriting"::: )   ; 
end; definitionlet "C" be   ($#l2_altcat_1 :::"category":::); attr "C" is  :::"concrete":::  means :: YELLOW18:def 11 (Bool  "("  (Bool "C" "is"   ($#v2_yellow18 :::"para-functional"::: )  ) & (Bool "C" "is"   ($#v9_altcat_1 :::"semi-functional"::: )  ) & (Bool "C" "is"   ($#v3_yellow18 :::"set-id-inheriting"::: )  )  ")" ); end; 




:: deftheorem    defines :::"concrete"::: YELLOW18:def 11 :  (Bool  "for" (Set (Var "C")) "being"   ($#l2_altcat_1 :::"category":::) "holds"   (Bool  "("  (Bool (Set (Var "C")) "is"   ($#v4_yellow18 :::"concrete"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "C")) "is"   ($#v2_yellow18 :::"para-functional"::: )  ) & (Bool (Set (Var "C")) "is"   ($#v9_altcat_1 :::"semi-functional"::: )  ) & (Bool (Set (Var "C")) "is"   ($#v3_yellow18 :::"set-id-inheriting"::: )  )  ")" )  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#v11_altcat_1 :::"associative"::: )     ($#v12_altcat_1 :::"with_units"::: )     ($#v4_yellow18 :::"concrete"::: )    ->   ($#v9_altcat_1 :::"semi-functional"::: )     ($#v2_yellow18 :::"para-functional"::: )     ($#v3_yellow18 :::"set-id-inheriting"::: )    for    ($#l2_altcat_1 :::"AltCatStr"::: )  ; 

cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#v9_altcat_1 :::"semi-functional"::: )     ($#v11_altcat_1 :::"associative"::: )     ($#v12_altcat_1 :::"with_units"::: )     ($#v2_yellow18 :::"para-functional"::: )     ($#v3_yellow18 :::"set-id-inheriting"::: )    ->   ($#v4_yellow18 :::"concrete"::: )    for    ($#l2_altcat_1 :::"AltCatStr"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#v6_altcat_1 :::"strict"::: )     ($#v8_altcat_1 :::"quasi-functional"::: )     ($#v11_altcat_1 :::"associative"::: )     ($#v12_altcat_1 :::"with_units"::: )     ($#v1_altcat_2 :::"reflexive"::: )     ($#v4_yellow18 :::"concrete"::: )    for    ($#l2_altcat_1 :::"AltCatStr"::: )  ; 
end; 
theorem :: YELLOW18:33 (Bool  "for" (Set (Var "C")) "being"   ($#l2_altcat_1 :::"category":::) "holds"   (Bool  "("  (Bool (Set (Var "C")) "is"   ($#v2_yellow18 :::"para-functional"::: )  ) "iff" (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds"  (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set  "("  ($#k3_yellow18 :::"the_carrier_of"::: )  (Set (Var "a1")) ")" ) "," (Set  "("  ($#k3_yellow18 :::"the_carrier_of"::: )  (Set (Var "a2")) ")" ) ")" )))  ")" )) ; 
 
theorem :: YELLOW18:34 (Bool  "for" (Set (Var "C")) "being"   ($#v2_yellow18 :::"para-functional"::: )    ($#l2_altcat_1 :::"category":::)  (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 (Var "f")) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k3_yellow18 :::"the_carrier_of"::: )  (Set (Var "a")) ")" ) "," (Set  "("  ($#k3_yellow18 :::"the_carrier_of"::: )  (Set (Var "b")) ")" ))))) ; 
 registrationlet "A" be   ($#v2_yellow18 :::"para-functional"::: )    ($#l2_altcat_1 :::"category":::); let "a", "b" be   ($#m1_subset_1 :::"object":::) "of" (Set (Const "A")); 
cluster   ->   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k1_altcat_1 :::"<^"::: ) "a" "," "b" ($#k1_altcat_1 :::"^>"::: ) ); 
end; 
theorem :: YELLOW18:35 (Bool  "for" (Set (Var "C")) "being"   ($#v2_yellow18 :::"para-functional"::: )    ($#l2_altcat_1 :::"category":::)  (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  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_yellow18 :::"the_carrier_of"::: )  (Set (Var "a")))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_yellow18 :::"the_carrier_of"::: )  (Set (Var "b"))))  ")" )))) ; 
 
theorem :: YELLOW18:36 (Bool  "for" (Set (Var "C")) "being"   ($#v9_altcat_1 :::"semi-functional"::: )     ($#v2_yellow18 :::"para-functional"::: )    ($#l2_altcat_1 :::"category":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "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 :::"{}"::: )  )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#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 "b")) "," (Set (Var "c")) "holds"  (Bool (Set (Set (Var "g"))  ($#k5_altcat_1 :::"*"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "f")))))))) ; 
 
theorem :: YELLOW18:37 (Bool  "for" (Set (Var "C")) "being"   ($#v9_altcat_1 :::"semi-functional"::: )     ($#v2_yellow18 :::"para-functional"::: )    ($#l2_altcat_1 :::"category":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set   ($#k6_partfun1 :::"id"::: )  (Set  "("  ($#k3_yellow18 :::"the_carrier_of"::: )  (Set (Var "a")) ")" ))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "a")) ($#k1_altcat_1 :::"^>"::: ) ))) "holds"  (Bool (Set   ($#k8_altcat_1 :::"idm"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set  "("  ($#k3_yellow18 :::"the_carrier_of"::: )  (Set (Var "a")) ")" ))))) ; 
 scheme  :: YELLOW18:sch 16 ConcreteCategoryLambda{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F3(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "ex" (Set (Var "C")) "being"   ($#v6_altcat_1 :::"strict"::: )     ($#v4_yellow18 :::"concrete"::: )    ($#l2_altcat_1 :::"category":::) "st"  (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds"  (Bool (Set   ($#k3_yellow18 :::"the_carrier_of"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "a")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds"  (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "b")) "," (Set (Var "c")) ")" ))) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "f")))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "c")) ")" ))))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"  (Bool (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set F3 "(" (Set (Var "a")) ")" ) "," (Set F3 "(" (Set (Var "b")) ")" ) ")" )))
 and  
(Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"  (Bool (Set   ($#k6_partfun1 :::"id"::: )  (Set F3 "(" (Set (Var "a")) ")" ))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "a")) ")" )))
 proof 


end; scheme  :: YELLOW18:sch 17 ConcreteCategoryQuasiLambda{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ], F2(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "ex" (Set (Var "C")) "being"   ($#v6_altcat_1 :::"strict"::: )     ($#v4_yellow18 :::"concrete"::: )    ($#l2_altcat_1 :::"category":::) "st"  (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds"  (Bool (Set   ($#k3_yellow18 :::"the_carrier_of"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "a")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set (Var "C")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set F2 "(" (Set (Var "a")) ")" ) "," (Set F2 "(" (Set (Var "b")) ")" ) ")" )) & (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))])  ")" )  ")" ))  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))]) & (Bool P1[(Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "g"))])) "holds"  (Bool P1[(Set (Var "a")) "," (Set (Var "c")) "," (Set (Set (Var "g"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "f")))])))
 and  
(Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"  (Bool P1[(Set (Var "a")) "," (Set (Var "a")) "," (Set   ($#k6_partfun1 :::"id"::: )  (Set F2 "(" (Set (Var "a")) ")" ))]))
 proof 


end; scheme  :: YELLOW18:sch 18 ConcreteCategoryEx{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "C")) "being"   ($#v6_altcat_1 :::"strict"::: )     ($#v4_yellow18 :::"concrete"::: )    ($#l2_altcat_1 :::"category":::) "st"  (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_yellow18 :::"the_carrier_of"::: )  (Set (Var "a")))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) ")" )) & (Bool P1[(Set (Var "a")) "," (Set (Var "x"))])  ")" )  ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set (Var "C")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set  "(" (Set (Var "C"))  ($#k3_yellow18 :::"-carrier_of"::: )  (Set (Var "a")) ")" ) "," (Set  "(" (Set (Var "C"))  ($#k3_yellow18 :::"-carrier_of"::: )  (Set (Var "b")) ")" ) ")" )) & (Bool P2[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))])  ")" )  ")" ))  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool P2[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))]) & (Bool P2[(Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "g"))])) "holds"  (Bool P2[(Set (Var "a")) "," (Set (Var "c")) "," (Set (Set (Var "g"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "f")))])))
 and  
(Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) ")" )) & (Bool P1[(Set (Var "a")) "," (Set (Var "x"))])  ")" )  ")" )  ")" )) "holds"  (Bool P2[(Set (Var "a")) "," (Set (Var "a")) "," (Set   ($#k6_partfun1 :::"id"::: )  (Set (Var "X")))])))
 proof 


end; scheme  :: YELLOW18:sch 19 ConcreteCategoryUniq1{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"   ($#v9_altcat_1 :::"semi-functional"::: )     ($#v2_yellow18 :::"para-functional"::: )    ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C1")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "holds"  (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))  ")" ) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C2")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C2")) "holds"  (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))  ")" )) "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"))) "#)" )))
 proof 


end; scheme  :: YELLOW18:sch 20 ConcreteCategoryUniq2{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ], F2(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"   ($#v9_altcat_1 :::"semi-functional"::: )     ($#v2_yellow18 :::"para-functional"::: )    ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C1")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set (Var "C1")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set F2 "(" (Set (Var "a")) ")" ) "," (Set F2 "(" (Set (Var "b")) ")" ) ")" )) & (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))])  ")" )  ")" ))  ")" ) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C2")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set (Var "C2")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set F2 "(" (Set (Var "a")) ")" ) "," (Set F2 "(" (Set (Var "b")) ")" ) ")" )) & (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))])  ")" )  ")" ))  ")" )) "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"))) "#)" )))
 proof 


end; scheme  :: YELLOW18:sch 21 ConcreteCategoryUniq3{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"   ($#v9_altcat_1 :::"semi-functional"::: )     ($#v2_yellow18 :::"para-functional"::: )    ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C1")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_yellow18 :::"the_carrier_of"::: )  (Set (Var "a")))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) ")" )) & (Bool P1[(Set (Var "a")) "," (Set (Var "x"))])  ")" )  ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set (Var "C1")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set  "(" (Set (Var "C1"))  ($#k3_yellow18 :::"-carrier_of"::: )  (Set (Var "a")) ")" ) "," (Set  "(" (Set (Var "C1"))  ($#k3_yellow18 :::"-carrier_of"::: )  (Set (Var "b")) ")" ) ")" )) & (Bool P2[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))])  ")" )  ")" ))  ")" ) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C2")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C2"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_yellow18 :::"the_carrier_of"::: )  (Set (Var "a")))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set F2 "(" (Set (Var "a")) ")" )) & (Bool P1[(Set (Var "a")) "," (Set (Var "x"))])  ")" )  ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set (Var "C2")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set  "(" (Set (Var "C2"))  ($#k3_yellow18 :::"-carrier_of"::: )  (Set (Var "a")) ")" ) "," (Set  "(" (Set (Var "C2"))  ($#k3_yellow18 :::"-carrier_of"::: )  (Set (Var "b")) ")" ) ")" )) & (Bool P2[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))])  ")" )  ")" ))  ")" )) "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"))) "#)" )))
 proof 


end; begin  
theorem :: YELLOW18:38 (Bool  "for" (Set (Var "C")) "being"   ($#v4_yellow18 :::"concrete"::: )    ($#l2_altcat_1 :::"category":::)  (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 :::"{}"::: )  )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#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"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v1_altcat_3 :::"retraction"::: )  )) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_yellow18 :::"the_carrier_of"::: )  (Set (Var "b"))))))) ; 
 
theorem :: YELLOW18:39 (Bool  "for" (Set (Var "C")) "being"   ($#v4_yellow18 :::"concrete"::: )    ($#l2_altcat_1 :::"category":::)  (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 :::"{}"::: )  )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#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"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_altcat_3 :::"coretraction"::: )  )) "holds"  (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )))) ; 
 
theorem :: YELLOW18:40 (Bool  "for" (Set (Var "C")) "being"   ($#v4_yellow18 :::"concrete"::: )    ($#l2_altcat_1 :::"category":::)  (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 :::"{}"::: )  )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#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"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_altcat_3 :::"iso"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_yellow18 :::"the_carrier_of"::: )  (Set (Var "b"))))  ")" )))) ; 
 
theorem :: YELLOW18:41 (Bool  "for" (Set (Var "C")) "being"   ($#v9_altcat_1 :::"semi-functional"::: )     ($#v2_yellow18 :::"para-functional"::: )    ($#l2_altcat_1 :::"category":::)  (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"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k2_funct_1 :::"""::: )  )  ($#r2_hidden :::"in"::: )  (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k1_altcat_1 :::"^>"::: ) ))) "holds"  (Bool (Set (Var "f")) "is"   ($#v3_altcat_3 :::"iso"::: )  )))) ; 
 
theorem :: YELLOW18:42 (Bool  "for" (Set (Var "C")) "being"   ($#v4_yellow18 :::"concrete"::: )    ($#l2_altcat_1 :::"category":::)  (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 :::"{}"::: )  )) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#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"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_altcat_3 :::"iso"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_altcat_3 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k2_funct_1 :::"""::: )  ))))) ; 
 scheme  :: YELLOW18:sch 22 ConcreteCatEquivalence{ F1() ->   ($#v9_altcat_1 :::"semi-functional"::: )     ($#v2_yellow18 :::"para-functional"::: )    ($#l2_altcat_1 :::"category":::), F2() ->   ($#v9_altcat_1 :::"semi-functional"::: )     ($#v2_yellow18 :::"para-functional"::: )    ($#l2_altcat_1 :::"category":::), F3(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F4(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F5(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->   ($#m1_hidden :::"Function":::), F6(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->   ($#m1_hidden :::"Function":::), F7(   ($#m1_hidden :::"set"::: )  ) ->   ($#m1_hidden :::"Function":::), F8(   ($#m1_hidden :::"set"::: )  ) ->   ($#m1_hidden :::"Function":::) } : 
(Bool (Set F1 "("  ")" ) "," (Set F2 "("  ")" )  ($#r1_yellow18 :::"are_equivalent"::: )  )
 provided
(Bool  "ex" (Set (Var "F")) "being"   ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_functor0 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "a")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "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 (Var "f")))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" )))  ")" )  ")" ))
 and  
(Bool  "ex" (Set (Var "G")) "being"   ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set F2 "("  ")" ) "," (Set F1 "("  ")" ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F2 "("  ")" ) "holds"  (Bool (Set (Set (Var "G"))  ($#k3_functor0 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "a")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F2 "("  ")" )  "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 (Var "f")))  ($#r1_hidden :::"="::: )  (Set F6 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" )))  ")" )  ")" ))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set F3 "(" (Set (Var "b")) ")" ) ")" ))) "holds"  (Bool  "("  (Bool (Set F7 "(" (Set (Var "b")) ")" )  ($#r2_hidden :::"in"::: )  (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) & (Bool (Set (Set F7 "(" (Set (Var "b")) ")" )  ($#k2_funct_1 :::"""::: )  )  ($#r2_hidden :::"in"::: )  (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k1_altcat_1 :::"^>"::: ) )) & (Bool (Set F7 "(" (Set (Var "b")) ")" ) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )  ")" ))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F2 "("  ")" )  "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set F4 "(" (Set (Var "a")) ")" ) ")" ))) "holds"  (Bool  "("  (Bool (Set F8 "(" (Set (Var "a")) ")" )  ($#r2_hidden :::"in"::: )  (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) & (Bool (Set (Set F8 "(" (Set (Var "a")) ")" )  ($#k2_funct_1 :::"""::: )  )  ($#r2_hidden :::"in"::: )  (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k1_altcat_1 :::"^>"::: ) )) & (Bool (Set F8 "(" (Set (Var "a")) ")" ) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )  ")" ))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F1 "("  ")" )  "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 F7 "(" (Set (Var "b")) ")" )  ($#k3_relat_1 :::"*"::: )  (Set F6 "(" (Set F3 "(" (Set (Var "a")) ")" ) "," (Set F3 "(" (Set (Var "b")) ")" ) "," (Set F5 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_relat_1 :::"*"::: )  (Set F7 "(" (Set (Var "a")) ")" )))))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set F2 "("  ")" )  "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 F5 "(" (Set F4 "(" (Set (Var "a")) ")" ) "," (Set F4 "(" (Set (Var "b")) ")" ) "," (Set F6 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" ) ")" )  ($#k3_relat_1 :::"*"::: )  (Set F8 "(" (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set F8 "(" (Set (Var "b")) ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "f"))))))
 proof 


end; begin  definitionlet "C" be   ($#l2_altcat_1 :::"category":::); func  :::"Concretized"::: "C" ->   ($#v6_altcat_1 :::"strict"::: )     ($#v4_yellow18 :::"concrete"::: )    ($#l2_altcat_1 :::"category":::) means :: YELLOW18:def 12 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "C")) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" it  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_yellow18 :::"the_carrier_of"::: )  (Set (Var "a")))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set  "("  ($#k2_card_3 :::"disjoin"::: )  (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" "C") ")" ))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k16_mcart_1 :::"`22"::: )  ))  ")" )  ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" "C"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" it)  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set  "(" it  ($#k3_yellow18 :::"-carrier_of"::: )  (Set (Var "a")) ")" ) "," (Set  "(" it  ($#k3_yellow18 :::"-carrier_of"::: )  (Set (Var "b")) ")" ) ")" )) & (Bool  "ex" (Set (Var "fa")) "," (Set (Var "fb")) "being"   ($#m1_subset_1 :::"object":::) "of" "C"(Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "fa")) "," (Set (Var "fb")) "st"  (Bool  "("  (Bool (Set (Var "fa"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "fb"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "fa")) "," (Set (Var "fb")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "("   "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"object":::) "of" "C"  "st" (Bool (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "fa")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o")) "," (Set (Var "fa")) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "h")) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set (Var "fa")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "g"))  ($#k5_altcat_1 :::"*"::: )  (Set (Var "h")) ")" ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set (Var "fb")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) )))  ")" )  ")" )))  ")" )  ")" ))  ")" )  ")" ); end; 





:: deftheorem    defines :::"Concretized"::: YELLOW18:def 12 :  (Bool  "for" (Set (Var "C")) "being"   ($#l2_altcat_1 :::"category":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#v6_altcat_1 :::"strict"::: )     ($#v4_yellow18 :::"concrete"::: )    ($#l2_altcat_1 :::"category":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_yellow18 :::"Concretized"::: )  (Set (Var "C")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C")))) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "b2"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_yellow18 :::"the_carrier_of"::: )  (Set (Var "a")))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set  "("  ($#k2_card_3 :::"disjoin"::: )  (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set (Var "C"))) ")" ))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k16_mcart_1 :::"`22"::: )  ))  ")" )  ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set (Var "b2")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set  "(" (Set (Var "b2"))  ($#k3_yellow18 :::"-carrier_of"::: )  (Set (Var "a")) ")" ) "," (Set  "(" (Set (Var "b2"))  ($#k3_yellow18 :::"-carrier_of"::: )  (Set (Var "b")) ")" ) ")" )) & (Bool  "ex" (Set (Var "fa")) "," (Set (Var "fb")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C"))(Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "fa")) "," (Set (Var "fb")) "st"  (Bool  "("  (Bool (Set (Var "fa"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "fb"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "fa")) "," (Set (Var "fb")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "("   "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "fa")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o")) "," (Set (Var "fa")) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "h")) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set (Var "fa")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "g"))  ($#k5_altcat_1 :::"*"::: )  (Set (Var "h")) ")" ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set (Var "fb")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) )))  ")" )  ")" )))  ")" )  ")" ))  ")" )  ")" )  ")" ))); 
 
theorem :: YELLOW18:43 (Bool  "for" (Set (Var "A")) "being"   ($#l2_altcat_1 :::"category":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k4_yellow18 :::"Concretized"::: )  (Set (Var "A")) ")" )  ($#k3_yellow18 :::"-carrier_of"::: )  (Set (Var "a")))) "iff" (Bool  "ex" (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "A"))(Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b")) "," (Set (Var "a")) "st"  (Bool  "("  (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "f")) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ))  ")" )))  ")" )))) ; 
 registrationlet "A" be   ($#l2_altcat_1 :::"category":::); let "a" be   ($#m1_subset_1 :::"object":::) "of" (Set (Const "A")); 
cluster (Set (Set  "("  ($#k4_yellow18 :::"Concretized"::: )  "A" ")" )  ($#k3_yellow18 :::"-carrier_of"::: )  "a") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: YELLOW18:44 (Bool  "for" (Set (Var "A")) "being"   ($#l2_altcat_1 :::"category":::)  (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")) (Bool  "ex" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k4_yellow18 :::"Concretized"::: )  (Set (Var "A")) ")" )  ($#k3_yellow18 :::"-carrier_of"::: )  (Set (Var "a")) ")" ) "," (Set  "(" (Set  "("  ($#k4_yellow18 :::"Concretized"::: )  (Set (Var "A")) ")" )  ($#k3_yellow18 :::"-carrier_of"::: )  (Set (Var "b")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "F"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set  "("  ($#k4_yellow18 :::"Concretized"::: )  (Set (Var "A")) ")" ))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool  "("   "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "c")) "," (Set (Var "a"))  "st" (Bool (Bool (Set  ($#k1_altcat_1 :::"<^"::: ) (Set (Var "c")) "," (Set (Var "a")) ($#k1_altcat_1 :::"^>"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "f"))  ($#k5_altcat_1 :::"*"::: )  (Set (Var "g")) ")" ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) )))  ")" )  ")" ))))) ; 
 
theorem :: YELLOW18:45 (Bool  "for" (Set (Var "A")) "being"   ($#l2_altcat_1 :::"category":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "F1"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set  "("  ($#k4_yellow18 :::"Concretized"::: )  (Set (Var "A")) ")" ))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "F2"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set  "("  ($#k4_yellow18 :::"Concretized"::: )  (Set (Var "A")) ")" ))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Set (Var "F1"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set  "("  ($#k8_altcat_1 :::"idm"::: )  (Set (Var "a")) ")" ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F2"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set  "("  ($#k8_altcat_1 :::"idm"::: )  (Set (Var "a")) ")" ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) )))) "holds"  (Bool (Set (Var "F1"))  ($#r1_hidden :::"="::: )  (Set (Var "F2")))))) ; 
 scheme  :: YELLOW18:sch 23 NonUniqMSFunctionEx{ F1() ->    ($#m1_hidden :::"set"::: )  , F2() ->   ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "("  ")" ), F3() ->   ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "F")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set F2 "("  ")" ) "," (Set F3 "("  ")" ) "st"  (Bool  "for" (Set (Var "i")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set F2 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r2_hidden :::"in"::: )  (Set (Set F3 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool P1[(Set (Var "i")) "," (Set (Var "x")) "," (Set (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))])  ")" )))
 provided
(Bool  "for" (Set (Var "i")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set F2 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))) "holds"  (Bool  "ex" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Set F3 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool P1[(Set (Var "i")) "," (Set (Var "x")) "," (Set (Var "y"))])  ")" )))
 proof 


end; definitionlet "A" be   ($#l2_altcat_1 :::"category":::); func  :::"Concretization"::: "A" ->   ($#v9_functor0 :::"strict"::: )     ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" "A" "," (Set   ($#k4_yellow18 :::"Concretized"::: )  "A") means :: YELLOW18:def 13 (Bool  "("  (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" "A" "holds"  (Bool (Set it  ($#k3_functor0 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"object":::) "of" "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  "(" it  ($#k6_functor0 :::"."::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set  "("  ($#k8_altcat_1 :::"idm"::: )  (Set (Var "a")) ")" ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "f")) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) )))  ")" )  ")" ); end; 





:: deftheorem    defines :::"Concretization"::: YELLOW18:def 13 :  (Bool  "for" (Set (Var "A")) "being"   ($#l2_altcat_1 :::"category":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#v9_functor0 :::"strict"::: )     ($#v15_functor0 :::"covariant"::: )     ($#m2_functor0 :::"Functor"::: )   "of" (Set (Var "A")) "," (Set   ($#k4_yellow18 :::"Concretized"::: )  (Set (Var "A"))) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_yellow18 :::"Concretization"::: )  (Set (Var "A")))) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set (Var "b2"))  ($#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  "(" (Set (Var "b2"))  ($#k6_functor0 :::"."::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set  "("  ($#k8_altcat_1 :::"idm"::: )  (Set (Var "a")) ")" ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "f")) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) )))  ")" )  ")" )  ")" ))); 
 registrationlet "A" be   ($#l2_altcat_1 :::"category":::); 
cluster (Set   ($#k5_yellow18 :::"Concretization"::: )  "A") ->   ($#v9_functor0 :::"strict"::: )     ($#v15_functor0 :::"covariant"::: )     ($#v21_functor0 :::"bijective"::: )   ; 
end; 
theorem :: YELLOW18:46 (Bool  "for" (Set (Var "A")) "being"   ($#l2_altcat_1 :::"category":::) "holds"  (Bool (Set (Var "A")) "," (Set   ($#k4_yellow18 :::"Concretized"::: )  (Set (Var "A")))  ($#r1_functor0 :::"are_isomorphic"::: )  )) ;