:: YELLOW21 semantic presentation begin definitionlet "a" be ($#m1_hidden :::"set"::: ) ; func "a" :::"as_1-sorted"::: -> ($#l1_struct_0 :::"1-sorted"::: ) equals :: YELLOW21:def 1 "a" if (Bool "a" "is" ($#l1_struct_0 :::"1-sorted"::: ) ) otherwise (Set ($#g1_struct_0 :::"1-sorted"::: ) "(#" "a" "#)" ); end; :: deftheorem defines :::"as_1-sorted"::: YELLOW21:def 1 : (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) "is" ($#l1_struct_0 :::"1-sorted"::: ) )) "implies" (Bool (Set (Set (Var "a")) ($#k1_yellow21 :::"as_1-sorted"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" & "(" (Bool (Bool (Set (Var "a")) "is" (Bool "not" ($#l1_struct_0 :::"1-sorted"::: ) ))) "implies" (Bool (Set (Set (Var "a")) ($#k1_yellow21 :::"as_1-sorted"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_struct_0 :::"1-sorted"::: ) "(#" (Set (Var "a")) "#)" )) ")" ")" )); definitionlet "W" be ($#m1_hidden :::"set"::: ) ; func :::"POSETS"::: "W" -> ($#m1_hidden :::"set"::: ) means :: YELLOW21:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_orders_2 :::"strict"::: ) ($#l1_orders_2 :::"Poset":::)) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "x")) ($#k1_yellow21 :::"as_1-sorted"::: ) ")" )) ($#r2_hidden :::"in"::: ) "W") ")" ) ")" )); end; :: deftheorem defines :::"POSETS"::: YELLOW21:def 2 : (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow21 :::"POSETS"::: ) (Set (Var "W")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_orders_2 :::"strict"::: ) ($#l1_orders_2 :::"Poset":::)) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "x")) ($#k1_yellow21 :::"as_1-sorted"::: ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) ")" ) ")" )) ")" ))); registrationlet "W" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_yellow21 :::"POSETS"::: ) "W") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "W" be ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_yellow21 :::"POSETS"::: ) "W") -> ($#v4_orders_3 :::"POSet_set-like"::: ) ; end; definitionlet "C" be ($#l2_altcat_1 :::"category":::); attr "C" is :::"carrier-underlaid"::: means :: YELLOW21:def 3 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" "C" (Bool "ex" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "S"))) & (Bool (Set ($#k3_yellow18 :::"the_carrier_of"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) ")" ))); end; :: deftheorem defines :::"carrier-underlaid"::: YELLOW21:def 3 : (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v1_yellow21 :::"carrier-underlaid"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "ex" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "S"))) & (Bool (Set ($#k3_yellow18 :::"the_carrier_of"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) ")" ))) ")" )); definitionlet "C" be ($#l2_altcat_1 :::"category":::); attr "C" is :::"lattice-wise"::: means :: YELLOW21:def 4 (Bool "(" (Bool "C" "is" ($#v9_altcat_1 :::"semi-functional"::: ) ) & (Bool "C" "is" ($#v3_yellow18 :::"set-id-inheriting"::: ) ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" "C" "holds" (Bool (Set (Var "a")) "is" ($#l1_orders_2 :::"LATTICE":::)) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" "C" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_orders_3 :::"MonFuncs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"lattice-wise"::: YELLOW21:def 4 : (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v2_yellow21 :::"lattice-wise"::: ) ) "iff" (Bool "(" (Bool (Set (Var "C")) "is" ($#v9_altcat_1 :::"semi-functional"::: ) ) & (Bool (Set (Var "C")) "is" ($#v3_yellow18 :::"set-id-inheriting"::: ) ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Var "a")) "is" ($#l1_orders_2 :::"LATTICE":::)) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_orders_3 :::"MonFuncs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ))) ")" ) ")" ) ")" )); definitionlet "C" be ($#l2_altcat_1 :::"category":::); attr "C" is :::"with_complete_lattices"::: means :: YELLOW21:def 5 (Bool "(" (Bool "C" "is" ($#v2_yellow21 :::"lattice-wise"::: ) ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" "C" "holds" (Bool (Set (Var "a")) "is" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::)) ")" ) ")" ); end; :: deftheorem defines :::"with_complete_lattices"::: YELLOW21:def 5 : (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v3_yellow21 :::"with_complete_lattices"::: ) ) "iff" (Bool "(" (Bool (Set (Var "C")) "is" ($#v2_yellow21 :::"lattice-wise"::: ) ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Var "a")) "is" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::)) ")" ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) bbbadV11_ALTCAT_1() ($#v12_altcat_1 :::"with_units"::: ) ($#v3_yellow21 :::"with_complete_lattices"::: ) -> ($#v2_yellow21 :::"lattice-wise"::: ) for ($#l2_altcat_1 :::"AltCatStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) bbbadV11_ALTCAT_1() ($#v12_altcat_1 :::"with_units"::: ) ($#v2_yellow21 :::"lattice-wise"::: ) -> ($#v4_yellow18 :::"concrete"::: ) ($#v1_yellow21 :::"carrier-underlaid"::: ) for ($#l2_altcat_1 :::"AltCatStr"::: ) ; end; scheme :: YELLOW21:sch 1 localCLCatEx{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#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 (Var "C")) "is" ($#v2_yellow21 :::"lattice-wise"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "a")) "," (Set (Var "b")) "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 "a")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))]) ")" ) ")" )) ")" ) ")" )) provided (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Var "a")) "is" ($#l1_orders_2 :::"LATTICE":::))) and (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "b")) "," (Set (Var "c")) "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")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")))])))) and (Bool "for" (Set (Var "a")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool P1[(Set (Var "a")) "," (Set (Var "a")) "," (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "a")))])) proof end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v6_altcat_1 :::"strict"::: ) bbbadV11_ALTCAT_1() ($#v12_altcat_1 :::"with_units"::: ) ($#v1_altcat_2 :::"reflexive"::: ) ($#v3_yellow21 :::"with_complete_lattices"::: ) for ($#l2_altcat_1 :::"AltCatStr"::: ) ; end; theorem :: YELLOW21:1 (Bool "for" (Set (Var "C")) "being" ($#v1_yellow21 :::"carrier-underlaid"::: ) ($#l2_altcat_1 :::"category":::) (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 "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "a")) ($#k1_yellow21 :::"as_1-sorted"::: ) ")" ))))) ; theorem :: YELLOW21:2 (Bool "for" (Set (Var "C")) "being" ($#v3_yellow18 :::"set-id-inheriting"::: ) ($#v1_yellow21 :::"carrier-underlaid"::: ) ($#l2_altcat_1 :::"category":::) (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 ($#k3_struct_0 :::"id"::: ) (Set "(" (Set (Var "a")) ($#k1_yellow21 :::"as_1-sorted"::: ) ")" ))))) ; notationlet "C" be ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::); let "a" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); synonym :::"latt"::: "a" for "C" :::"as_1-sorted"::: ; end; definitionlet "C" be ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::); let "a" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); :: original: :::"as_1-sorted"::: redefine func :::"latt"::: "a" -> ($#l1_orders_2 :::"LATTICE":::) equals :: YELLOW21:def 6 "a"; end; :: deftheorem defines :::"latt"::: YELLOW21:def 6 : (Bool "for" (Set (Var "C")) "being" ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k3_yellow21 :::"latt"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))); notationlet "C" be ($#v3_yellow21 :::"with_complete_lattices"::: ) ($#l2_altcat_1 :::"category":::); let "a" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); synonym :::"latt"::: "a" for "C" :::"as_1-sorted"::: ; end; definitionlet "C" be ($#v3_yellow21 :::"with_complete_lattices"::: ) ($#l2_altcat_1 :::"category":::); let "a" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); :: original: :::"as_1-sorted"::: redefine func :::"latt"::: "a" -> ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); end; definitionlet "C" be ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::); let "a", "b" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); assume (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Const "a")) "," (Set (Const "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; let "f" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "a")) "," (Set (Const "b")); func :::"@"::: "f" -> ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_yellow21 :::"latt"::: ) "a" ")" ) "," (Set "(" ($#k3_yellow21 :::"latt"::: ) "b" ")" ) equals :: YELLOW21:def 7 "f"; end; :: deftheorem defines :::"@"::: YELLOW21:def 7 : (Bool "for" (Set (Var "C")) "being" ($#v2_yellow21 :::"lattice-wise"::: ) ($#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 ($#k5_yellow21 :::"@"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))))); theorem :: YELLOW21:3 (Bool "for" (Set (Var "C")) "being" ($#v2_yellow21 :::"lattice-wise"::: ) ($#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 "(" ($#k5_yellow21 :::"@"::: ) (Set (Var "g")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k5_yellow21 :::"@"::: ) (Set (Var "f")) ")" ))))))) ; scheme :: YELLOW21:sch 2 CLCatEx1{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "C")) "being" ($#v6_altcat_1 :::"strict"::: ) ($#v2_yellow21 :::"lattice-wise"::: ) ($#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" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "b")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool P1[(Set ($#k3_yellow21 :::"latt"::: ) (Set (Var "a"))) "," (Set ($#k3_yellow21 :::"latt"::: ) (Set (Var "b"))) "," (Set (Var "f"))]) ")" )) ")" ) ")" )) provided (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Var "a")) "is" ($#l1_orders_2 :::"LATTICE":::))) and (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "b")) "," (Set (Var "c")) "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")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")))])))) and (Bool "for" (Set (Var "a")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool P1[(Set (Var "a")) "," (Set (Var "a")) "," (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "a")))])) proof end; scheme :: YELLOW21:sch 3 CLCatEx2{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "C")) "being" ($#v6_altcat_1 :::"strict"::: ) ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C"))) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_orders_2 :::"strict"::: ) ) & (Bool P1[(Set (Var "x"))]) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (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" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "b")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool P2[(Set ($#k3_yellow21 :::"latt"::: ) (Set (Var "a"))) "," (Set ($#k3_yellow21 :::"latt"::: ) (Set (Var "b"))) "," (Set (Var "f"))]) ")" )) ")" ) ")" )) provided (Bool "ex" (Set (Var "x")) "being" ($#v1_orders_2 :::"strict"::: ) ($#l1_orders_2 :::"LATTICE":::) "st" (Bool "(" (Bool P1[(Set (Var "x"))]) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) ")" )) and (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool P1[(Set (Var "a"))]) & (Bool P1[(Set (Var "b"))]) & (Bool P1[(Set (Var "c"))])) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "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")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")))])))) and (Bool "for" (Set (Var "a")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool P1[(Set (Var "a"))])) "holds" (Bool P2[(Set (Var "a")) "," (Set (Var "a")) "," (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "a")))])) proof end; scheme :: YELLOW21:sch 4 CLCatUniq1{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#v2_yellow21 :::"lattice-wise"::: ) ($#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")) (Bool "for" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "b")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (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 :::"object":::) "of" (Set (Var "C2")) (Bool "for" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "b")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (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 :: YELLOW21:sch 5 CLCatUniq2{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1"))) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_orders_2 :::"strict"::: ) ) & (Bool P1[(Set (Var "x"))]) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) (Bool "for" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "b")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool P2[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))]) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C2"))) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_orders_2 :::"strict"::: ) ) & (Bool P1[(Set (Var "x"))]) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C2")) (Bool "for" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "b")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (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; scheme :: YELLOW21:sch 6 CLCovariantFunctorEx{ P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], F1() -> ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::), F2() -> ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::), F3( ($#m1_hidden :::"set"::: ) ) -> ($#l1_orders_2 :::"LATTICE":::), F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"Function":::) } : (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 "(" ($#k3_yellow21 :::"latt"::: ) (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 "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "b")) ")" ) "," (Set "(" ($#k5_yellow21 :::"@"::: ) (Set (Var "f")) ")" ) ")" ))) ")" ) ")" )) provided (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set F1 "(" ")" )) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" ))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" ))) & (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))]) ")" ) ")" ))) and (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set F2 "(" ")" )) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F2 "(" ")" ))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F2 "(" ")" ))) & (Bool P2[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))]) ")" ) ")" ))) and (Bool "for" (Set (Var "a")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" )))) "holds" (Bool (Set F3 "(" (Set (Var "a")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F2 "(" ")" )))) and (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))])) "holds" (Bool "(" (Bool (Set F4 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set F3 "(" (Set (Var "a")) ")" ) "," (Set F3 "(" (Set (Var "b")) ")" )) & (Bool P2[(Set F3 "(" (Set (Var "a")) ")" ) "," (Set F3 "(" (Set (Var "b")) ")" ) "," (Set F4 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" )]) ")" ))) and (Bool "for" (Set (Var "a")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" )))) "holds" (Bool (Set F4 "(" (Set (Var "a")) "," (Set (Var "a")) "," (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "a")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set F3 "(" (Set (Var "a")) ")" )))) and (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "b")) "," (Set (Var "c")) "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 (Set F4 "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "g")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set F4 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" )))))) proof end; scheme :: YELLOW21:sch 7 CLContravariantFunctorEx{ P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], F1() -> ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::), F2() -> ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::), F3( ($#m1_hidden :::"set"::: ) ) -> ($#l1_orders_2 :::"LATTICE":::), F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"Function":::) } : (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 "(" ($#k3_yellow21 :::"latt"::: ) (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 "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "b")) ")" ) "," (Set "(" ($#k5_yellow21 :::"@"::: ) (Set (Var "f")) ")" ) ")" ))) ")" ) ")" )) provided (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set F1 "(" ")" )) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" ))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" ))) & (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))]) ")" ) ")" ))) and (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set F2 "(" ")" )) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F2 "(" ")" ))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F2 "(" ")" ))) & (Bool P2[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))]) ")" ) ")" ))) and (Bool "for" (Set (Var "a")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" )))) "holds" (Bool (Set F3 "(" (Set (Var "a")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F2 "(" ")" )))) and (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))])) "holds" (Bool "(" (Bool (Set F4 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set F3 "(" (Set (Var "b")) ")" ) "," (Set F3 "(" (Set (Var "a")) ")" )) & (Bool P2[(Set F3 "(" (Set (Var "b")) ")" ) "," (Set F3 "(" (Set (Var "a")) ")" ) "," (Set F4 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" )]) ")" ))) and (Bool "for" (Set (Var "a")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" )))) "holds" (Bool (Set F4 "(" (Set (Var "a")) "," (Set (Var "a")) "," (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "a")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set F3 "(" (Set (Var "a")) ")" )))) and (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "b")) "," (Set (Var "c")) "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 (Set F4 "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set F4 "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "g")) ")" )))))) proof end; scheme :: YELLOW21:sch 8 CLCatIsomorphism{ P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], F1() -> ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::), F2() -> ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::), F3( ($#m1_hidden :::"set"::: ) ) -> ($#l1_orders_2 :::"LATTICE":::), F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"Function":::) } : (Bool (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#r1_functor0 :::"are_isomorphic"::: ) ) provided (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set F1 "(" ")" )) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" ))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" ))) & (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))]) ")" ) ")" ))) and (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set F2 "(" ")" )) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F2 "(" ")" ))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F2 "(" ")" ))) & (Bool P2[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))]) ")" ) ")" ))) and (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" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" ))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" ))) & (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" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))]) & (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "g"))]) & (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")) ($#r2_funct_2 :::"="::: ) (Set (Var "g"))))) and (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool P2[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))])) "holds" (Bool "ex" (Set (Var "c")) "," (Set (Var "d")) "being" ($#l1_orders_2 :::"LATTICE":::)(Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "c")) "," (Set (Var "d")) "st" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" ))) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" ))) & (Bool P1[(Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "g"))]) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "c")) ")" )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "d")) ")" )) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "g")) ")" )) ")" ))))) proof end; scheme :: YELLOW21:sch 9 CLCatAntiIsomorphism{ P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], F1() -> ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::), F2() -> ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::), F3( ($#m1_hidden :::"set"::: ) ) -> ($#l1_orders_2 :::"LATTICE":::), F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"Function":::) } : (Bool (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#r2_functor0 :::"are_anti-isomorphic"::: ) ) provided (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set F1 "(" ")" )) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" ))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" ))) & (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))]) ")" ) ")" ))) and (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set F2 "(" ")" )) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F2 "(" ")" ))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F2 "(" ")" ))) & (Bool P2[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))]) ")" ) ")" ))) and (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" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" ))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" ))) & (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" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "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")) ($#r2_funct_2 :::"="::: ) (Set (Var "g"))))) and (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool P2[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))])) "holds" (Bool "ex" (Set (Var "c")) "," (Set (Var "d")) "being" ($#l1_orders_2 :::"LATTICE":::)(Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "c")) "," (Set (Var "d")) "st" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" ))) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" ))) & (Bool P1[(Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "g"))]) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "c")) ")" )) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "d")) ")" )) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "g")) ")" )) ")" ))))) proof end; begin definitionlet "C" be ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::); attr "C" is :::"with_all_isomorphisms"::: means :: YELLOW21:def 8 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" "C" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "b")) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) )) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )))); end; :: deftheorem defines :::"with_all_isomorphisms"::: YELLOW21:def 8 : (Bool "for" (Set (Var "C")) "being" ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v4_yellow21 :::"with_all_isomorphisms"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "b")) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) )) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v6_altcat_1 :::"strict"::: ) ($#v9_altcat_1 :::"semi-functional"::: ) bbbadV11_ALTCAT_1() ($#v12_altcat_1 :::"with_units"::: ) ($#v1_altcat_2 :::"reflexive"::: ) ($#v2_yellow18 :::"para-functional"::: ) ($#v3_yellow18 :::"set-id-inheriting"::: ) ($#v4_yellow18 :::"concrete"::: ) ($#v1_yellow21 :::"carrier-underlaid"::: ) ($#v2_yellow21 :::"lattice-wise"::: ) ($#v4_yellow21 :::"with_all_isomorphisms"::: ) for ($#l2_altcat_1 :::"AltCatStr"::: ) ; end; theorem :: YELLOW21:4 (Bool "for" (Set (Var "C")) "being" ($#v2_yellow21 :::"lattice-wise"::: ) ($#v4_yellow21 :::"with_all_isomorphisms"::: ) ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set ($#k5_yellow21 :::"@"::: ) (Set (Var "f"))) "is" ($#v23_waybel_0 :::"isomorphic"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v3_altcat_3 :::"iso"::: ) )))) ; theorem :: YELLOW21:5 (Bool "for" (Set (Var "C")) "being" ($#v2_yellow21 :::"lattice-wise"::: ) ($#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 ($#k5_yellow21 :::"@"::: ) (Set (Var "f"))) "is" ($#v23_waybel_0 :::"isomorphic"::: ) )))) ; scheme :: YELLOW21:sch 10 CLCatEquivalence{ P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], F1() -> ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::), F2() -> ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::), F3( ($#m1_hidden :::"set"::: ) ) -> ($#l1_orders_2 :::"LATTICE":::), F4( ($#m1_hidden :::"set"::: ) ) -> ($#l1_orders_2 :::"LATTICE":::), 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 "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "b")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool P1[(Set ($#k3_yellow21 :::"latt"::: ) (Set (Var "a"))) "," (Set ($#k3_yellow21 :::"latt"::: ) (Set (Var "b"))) "," (Set (Var "f"))]) ")" ))) and (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set F2 "(" ")" ) (Bool "for" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "b")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool P2[(Set ($#k3_yellow21 :::"latt"::: ) (Set (Var "a"))) "," (Set ($#k3_yellow21 :::"latt"::: ) (Set (Var "b"))) "," (Set (Var "f"))]) ")" ))) and (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")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" )))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set F4 "(" (Set F3 "(" (Set (Var "a")) ")" ) ")" ) "," (Set (Var "a")) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "a")) ")" )) & (Bool (Set (Var "f")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) ) & (Bool P1[(Set F4 "(" (Set F3 "(" (Set (Var "a")) ")" ) ")" ) "," (Set (Var "a")) "," (Set (Var "f"))]) & (Bool P1[(Set (Var "a")) "," (Set F4 "(" (Set F3 "(" (Set (Var "a")) ")" ) ")" ) "," (Set (Set (Var "f")) ($#k2_funct_1 :::"""::: ) )]) ")" ))) and (Bool "for" (Set (Var "a")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F2 "(" ")" )))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "a")) "," (Set F3 "(" (Set F4 "(" (Set (Var "a")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "a")) ")" )) & (Bool (Set (Var "f")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) ) & (Bool P2[(Set (Var "a")) "," (Set F3 "(" (Set F4 "(" (Set (Var "a")) ")" ) ")" ) "," (Set (Var "f"))]) & (Bool P2[(Set F3 "(" (Set F4 "(" (Set (Var "a")) ")" ) ")" ) "," (Set (Var "a")) "," (Set (Set (Var "f")) ($#k2_funct_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")) "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 "(" ($#k5_yellow21 :::"@"::: ) (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 "(" ($#k5_yellow21 :::"@"::: ) (Set (Var "f")) ")" ))))) proof end; begin definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"upper-bounded"::: means :: YELLOW21:def 9 (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) "R"))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R"))); end; :: deftheorem defines :::"upper-bounded"::: YELLOW21:def 9 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v5_yellow21 :::"upper-bounded"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))))) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_wellord1 :::"well-ordering"::: ) -> ($#v1_wellord1 :::"well_founded"::: ) ($#v1_relat_2 :::"reflexive"::: ) ($#v4_relat_2 :::"antisymmetric"::: ) ($#v6_relat_2 :::"connected"::: ) ($#v8_relat_2 :::"transitive"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_wellord1 :::"well-ordering"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: YELLOW21:6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ")" ))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" )))) ; registrationlet "f" be ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"Function":::); let "R" be ($#v1_relat_2 :::"reflexive"::: ) ($#m1_hidden :::"Relation":::); cluster (Set (Set "(" "f" ($#k3_relat_1 :::"*"::: ) "R" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" "f" ($#k2_funct_1 :::"""::: ) ")" )) -> ($#v1_relat_2 :::"reflexive"::: ) ; end; registrationlet "f" be ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"Function":::); let "R" be ($#v4_relat_2 :::"antisymmetric"::: ) ($#m1_hidden :::"Relation":::); cluster (Set (Set "(" "f" ($#k3_relat_1 :::"*"::: ) "R" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" "f" ($#k2_funct_1 :::"""::: ) ")" )) -> ($#v4_relat_2 :::"antisymmetric"::: ) ; end; registrationlet "f" be ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"Function":::); let "R" be ($#v8_relat_2 :::"transitive"::: ) ($#m1_hidden :::"Relation":::); cluster (Set (Set "(" "f" ($#k3_relat_1 :::"*"::: ) "R" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" "f" ($#k2_funct_1 :::"""::: ) ")" )) -> ($#v8_relat_2 :::"transitive"::: ) ; end; theorem :: YELLOW21:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "X")) "," (Set (Var "A")) ($#r2_wellord2 :::"are_equipotent"::: ) )) "holds" (Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "R")) ($#r2_wellord1 :::"well_orders"::: ) (Set (Var "X"))) & (Bool (Set ($#k2_wellord2 :::"order_type_of"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" )))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) ($#v2_wellord1 :::"well-ordering"::: ) bbbadV1_PARTFUN1("X") ($#v1_funct_2 :::"quasi_total"::: ) ($#v1_relat_2 :::"reflexive"::: ) ($#v4_relat_2 :::"antisymmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) ($#v5_yellow21 :::"upper-bounded"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "X" ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: YELLOW21:8 (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v2_yellow_0 :::"upper-bounded"::: ) ) "iff" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P"))) "is" ($#v5_yellow21 :::"upper-bounded"::: ) ) ")" )) ; theorem :: YELLOW21:9 (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"Poset":::) "st" (Bool (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P"))) "is" ($#v2_wellord1 :::"well-ordering"::: ) )) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v16_waybel_0 :::"connected"::: ) ) & (Bool (Set (Var "P")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set (Var "P")) "is" ($#v3_waybel_3 :::"continuous"::: ) ) ")" )) ; theorem :: YELLOW21:10 (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"Poset":::) "st" (Bool (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P"))) "is" ($#v2_wellord1 :::"well-ordering"::: ) )) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "y")) ($#r2_orders_2 :::"<"::: ) (Set (Var "x")))) "holds" (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool "(" (Bool (Set (Var "z")) "is" ($#v1_waybel_3 :::"compact"::: ) ) & (Bool (Set (Var "y")) ($#r3_orders_2 :::"<="::: ) (Set (Var "z"))) & (Bool (Set (Var "z")) ($#r3_orders_2 :::"<="::: ) (Set (Var "x"))) ")" )))) ; theorem :: YELLOW21:11 (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"Poset":::) "st" (Bool (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P"))) "is" ($#v2_wellord1 :::"well-ordering"::: ) )) "holds" (Bool (Set (Var "P")) "is" ($#v2_waybel_8 :::"algebraic"::: ) )) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#v2_wellord1 :::"well-ordering"::: ) ($#v5_yellow21 :::"upper-bounded"::: ) ($#m1_subset_1 :::"Order":::) "of" (Set (Const "X")); cluster (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" "X" "," "R" "#)" ) -> ($#v2_waybel_8 :::"algebraic"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v16_waybel_0 :::"connected"::: ) ($#v3_waybel_3 :::"continuous"::: ) ; end; definitionlet "W" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; given "w" being ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "W")) such that (Bool (Bool "not" (Set (Const "w")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ; func "W" :::"-UPS_category"::: -> ($#v6_altcat_1 :::"strict"::: ) ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::) means :: YELLOW21:def 10 (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"object":::) "of" it) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_orders_2 :::"strict"::: ) ) & (Bool (Set (Var "x")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "x"))) ($#r2_hidden :::"in"::: ) "W") ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" it (Bool "for" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "b")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool (Set (Var "f")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"-UPS_category"::: YELLOW21:def 10 : (Bool "for" (Set (Var "W")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "not" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "W")) "holds" (Bool (Set (Var "w")) "is" ($#v1_xboole_0 :::"empty"::: ) )))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#v6_altcat_1 :::"strict"::: ) ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k6_yellow21 :::"-UPS_category"::: ) )) "iff" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"object":::) "of" (Set (Var "b2"))) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_orders_2 :::"strict"::: ) ) & (Bool (Set (Var "x")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "b2")) (Bool "for" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "b")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool (Set (Var "f")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) ")" )) ")" ) ")" ) ")" ))); registrationlet "W" be ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "W" ($#k6_yellow21 :::"-UPS_category"::: ) ) -> ($#v6_altcat_1 :::"strict"::: ) ($#v2_yellow21 :::"lattice-wise"::: ) ($#v3_yellow21 :::"with_complete_lattices"::: ) ($#v4_yellow21 :::"with_all_isomorphisms"::: ) ; end; theorem :: YELLOW21:12 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "W")) ($#k6_yellow21 :::"-UPS_category"::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_yellow21 :::"POSETS"::: ) (Set (Var "W"))))) ; theorem :: YELLOW21:13 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k6_yellow21 :::"-UPS_category"::: ) ")" )) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::)) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_yellow21 :::"POSETS"::: ) (Set (Var "W")))) ")" ) ")" ))) ; theorem :: YELLOW21:14 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k6_yellow21 :::"-UPS_category"::: ) ")" )) "iff" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_orders_2 :::"strict"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_lattice3 :::"complete"::: ) ) ")" ) ")" ))) ; theorem :: YELLOW21:15 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k6_yellow21 :::"-UPS_category"::: ) ")" ) (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 (Set (Var "f")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k4_yellow21 :::"latt"::: ) (Set (Var "b")) ")" )) ")" )))) ; registrationlet "W" be ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) ; let "a", "b" be ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Const "W")) ($#k6_yellow21 :::"-UPS_category"::: ) ")" ); cluster (Set ($#k1_altcat_1 :::"<^"::: ) "a" "," "b" ($#k1_altcat_1 :::"^>"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; begin registrationlet "A" be ($#v3_yellow18 :::"set-id-inheriting"::: ) ($#l2_altcat_1 :::"category":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v3_altcat_2 :::"id-inheriting"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_yellow18 :::"set-id-inheriting"::: ) for ($#m1_altcat_2 :::"SubCatStr"::: ) "of" "A"; end; registrationlet "A" be ($#v2_yellow18 :::"para-functional"::: ) ($#l2_altcat_1 :::"category":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v3_altcat_2 :::"id-inheriting"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_yellow18 :::"para-functional"::: ) for ($#m1_altcat_2 :::"SubCatStr"::: ) "of" "A"; end; registrationlet "A" be ($#v9_altcat_1 :::"semi-functional"::: ) ($#l2_altcat_1 :::"category":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v9_altcat_1 :::"semi-functional"::: ) for ($#m1_altcat_2 :::"SubCatStr"::: ) "of" "A"; end; registrationlet "A" be ($#v1_yellow21 :::"carrier-underlaid"::: ) ($#l2_altcat_1 :::"category":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v3_altcat_2 :::"id-inheriting"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_yellow21 :::"carrier-underlaid"::: ) for ($#m1_altcat_2 :::"SubCatStr"::: ) "of" "A"; end; registrationlet "A" be ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v3_altcat_2 :::"id-inheriting"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_yellow21 :::"lattice-wise"::: ) for ($#m1_altcat_2 :::"SubCatStr"::: ) "of" "A"; end; registrationlet "A" be ($#v2_yellow21 :::"lattice-wise"::: ) ($#v4_yellow21 :::"with_all_isomorphisms"::: ) ($#l2_altcat_1 :::"category":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v2_altcat_2 :::"full"::: ) ($#v3_altcat_2 :::"id-inheriting"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow21 :::"with_all_isomorphisms"::: ) for ($#m1_altcat_2 :::"SubCatStr"::: ) "of" "A"; end; registrationlet "A" be ($#v3_yellow21 :::"with_complete_lattices"::: ) ($#l2_altcat_1 :::"category":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v3_altcat_2 :::"id-inheriting"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_yellow21 :::"with_complete_lattices"::: ) for ($#m1_altcat_2 :::"SubCatStr"::: ) "of" "A"; end; definitionlet "W" be ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) ; func "W" :::"-CONT_category"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_altcat_1 :::"strict"::: ) ($#v2_altcat_2 :::"full"::: ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set "W" ($#k6_yellow21 :::"-UPS_category"::: ) ) means :: YELLOW21:def 11 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" "W" ($#k6_yellow21 :::"-UPS_category"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"object":::) "of" it) "iff" (Bool (Set ($#k4_yellow21 :::"latt"::: ) (Set (Var "a"))) "is" ($#v3_waybel_3 :::"continuous"::: ) ) ")" )); end; :: deftheorem defines :::"-CONT_category"::: YELLOW21:def 11 : (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_altcat_1 :::"strict"::: ) ($#v2_altcat_2 :::"full"::: ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Set (Var "W")) ($#k6_yellow21 :::"-UPS_category"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k7_yellow21 :::"-CONT_category"::: ) )) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k6_yellow21 :::"-UPS_category"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"object":::) "of" (Set (Var "b2"))) "iff" (Bool (Set ($#k4_yellow21 :::"latt"::: ) (Set (Var "a"))) "is" ($#v3_waybel_3 :::"continuous"::: ) ) ")" )) ")" ))); definitionlet "W" be ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) ; func "W" :::"-ALG_category"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_altcat_1 :::"strict"::: ) ($#v2_altcat_2 :::"full"::: ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set "W" ($#k7_yellow21 :::"-CONT_category"::: ) ) means :: YELLOW21:def 12 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" "W" ($#k7_yellow21 :::"-CONT_category"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"object":::) "of" it) "iff" (Bool (Set ($#k4_yellow21 :::"latt"::: ) (Set (Var "a"))) "is" ($#v2_waybel_8 :::"algebraic"::: ) ) ")" )); end; :: deftheorem defines :::"-ALG_category"::: YELLOW21:def 12 : (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_altcat_1 :::"strict"::: ) ($#v2_altcat_2 :::"full"::: ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Set (Var "W")) ($#k7_yellow21 :::"-CONT_category"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k8_yellow21 :::"-ALG_category"::: ) )) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k7_yellow21 :::"-CONT_category"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"object":::) "of" (Set (Var "b2"))) "iff" (Bool (Set ($#k4_yellow21 :::"latt"::: ) (Set (Var "a"))) "is" ($#v2_waybel_8 :::"algebraic"::: ) ) ")" )) ")" ))); theorem :: YELLOW21:16 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k7_yellow21 :::"-CONT_category"::: ) ")" )) "iff" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_orders_2 :::"strict"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) ) ")" ) ")" ))) ; theorem :: YELLOW21:17 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k8_yellow21 :::"-ALG_category"::: ) ")" )) "iff" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_orders_2 :::"strict"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set (Var "L")) "is" ($#v2_waybel_8 :::"algebraic"::: ) ) ")" ) ")" ))) ; theorem :: YELLOW21:18 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k7_yellow21 :::"-CONT_category"::: ) ")" ) (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 (Set (Var "f")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k4_yellow21 :::"latt"::: ) (Set (Var "b")) ")" )) ")" )))) ; theorem :: YELLOW21:19 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k8_yellow21 :::"-ALG_category"::: ) ")" ) (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 (Set (Var "f")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k4_yellow21 :::"latt"::: ) (Set (Var "b")) ")" )) ")" )))) ; registrationlet "W" be ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) ; let "a", "b" be ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Const "W")) ($#k7_yellow21 :::"-CONT_category"::: ) ")" ); cluster (Set ($#k1_altcat_1 :::"<^"::: ) "a" "," "b" ($#k1_altcat_1 :::"^>"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "W" be ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) ; let "a", "b" be ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Const "W")) ($#k8_yellow21 :::"-ALG_category"::: ) ")" ); cluster (Set ($#k1_altcat_1 :::"<^"::: ) "a" "," "b" ($#k1_altcat_1 :::"^>"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end;