:: ORDERS_3 semantic presentation begin definitionlet "IT" be ($#l1_orders_2 :::"RelStr"::: ) ; attr "IT" is :::"discrete"::: means :: ORDERS_3:def 1 (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "IT") ($#r2_relset_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT"))); end; :: deftheorem defines :::"discrete"::: ORDERS_3:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_orders_3 :::"discrete"::: ) ) "iff" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "IT"))) ($#r2_relset_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) bbbadV2_ORDERS_2() ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_orders_3 :::"discrete"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) "#)" ) -> ($#v2_struct_0 :::"empty"::: ) ; let "P" be ($#v2_struct_0 :::"empty"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "P") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registration cluster ($#v2_struct_0 :::"empty"::: ) -> ($#v1_orders_3 :::"discrete"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; definitionlet "P" be ($#l1_orders_2 :::"RelStr"::: ) ; let "IT" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "P")); attr "IT" is :::"disconnected"::: means :: ORDERS_3:def 2 (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "P" "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "IT" ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")))) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "P") ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "P") ($#k2_wellord1 :::"|_2"::: ) (Set (Var "A")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "P") ($#k2_wellord1 :::"|_2"::: ) (Set (Var "B")) ")" ))) ")" )); end; :: deftheorem defines :::"disconnected"::: ORDERS_3:def 2 : (Bool "for" (Set (Var "P")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "P")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_orders_3 :::"disconnected"::: ) ) "iff" (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "P")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "IT")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")))) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P"))) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "A")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P"))) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "B")) ")" ))) ")" )) ")" ))); notationlet "P" be ($#l1_orders_2 :::"RelStr"::: ) ; let "IT" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "P")); antonym :::"connected"::: "IT" for :::"disconnected"::: ; end; definitionlet "IT" be ($#l1_orders_2 :::"RelStr"::: ) ; attr "IT" is :::"disconnected"::: means :: ORDERS_3:def 3 (Bool (Set ($#k2_struct_0 :::"[#]"::: ) "IT") "is" ($#v2_orders_3 :::"disconnected"::: ) ); end; :: deftheorem defines :::"disconnected"::: ORDERS_3:def 3 : (Bool "for" (Set (Var "IT")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_orders_3 :::"disconnected"::: ) ) "iff" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "IT"))) "is" ($#v2_orders_3 :::"disconnected"::: ) ) ")" )); notationlet "IT" be ($#l1_orders_2 :::"RelStr"::: ) ; antonym :::"connected"::: "IT" for :::"disconnected"::: ; end; theorem :: ORDERS_3:1 (Bool "for" (Set (Var "DP")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_3 :::"discrete"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "DP")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ))) ; theorem :: ORDERS_3:2 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#m1_subset_1 :::"Order":::) "of" (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: ORDERS_3:3 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v3_orders_2 :::"reflexive"::: ) ) & (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ))) "holds" (Bool (Set (Var "T")) "is" ($#v1_orders_3 :::"discrete"::: ) ))) ; theorem :: ORDERS_3:4 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Var "T")) "is" ($#v3_orders_3 :::"connected"::: ) ))) ; theorem :: ORDERS_3:5 (Bool "for" (Set (Var "DP")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_3 :::"discrete"::: ) ($#l1_orders_2 :::"Poset":::) "st" (Bool (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "DP")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "DP")) "is" ($#v3_orders_3 :::"disconnected"::: ) )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) bbbadV2_ORDERS_2() ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_orders_3 :::"connected"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) bbbadV2_ORDERS_2() ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_orders_3 :::"discrete"::: ) ($#v3_orders_3 :::"disconnected"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; begin definitionlet "IT" be ($#m1_hidden :::"set"::: ) ; attr "IT" is :::"POSet_set-like"::: means :: ORDERS_3:def 4 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool (Set (Var "a")) "is" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::))); end; :: deftheorem defines :::"POSet_set-like"::: ORDERS_3:def 4 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_orders_3 :::"POSet_set-like"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set (Var "a")) "is" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::))) ")" )); registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_orders_3 :::"POSet_set-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode POSet_set is ($#v4_orders_3 :::"POSet_set-like"::: ) ($#m1_hidden :::"set"::: ) ; end; definitionlet "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"POSet_set":::); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "P" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); end; definitionlet "L1", "L2" be ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "L1")) "," (Set (Const "L2")); attr "f" is :::"monotone"::: means :: ORDERS_3:def 5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L1" "st" (Bool (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "L2" "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))))); end; :: deftheorem defines :::"monotone"::: ORDERS_3:def 5 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "st" (Bool (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L2")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))))) ")" ))); definitionlet "A", "B" be ($#l1_orders_2 :::"RelStr"::: ) ; func :::"MonFuncs"::: "(" "A" "," "B" ")" -> ($#m1_hidden :::"set"::: ) means :: ORDERS_3:def 6 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" "A" "," "B" "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "B") ")" )) & (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) ) ")" )) ")" )); end; :: deftheorem defines :::"MonFuncs"::: ORDERS_3:def 6 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_orders_3 :::"MonFuncs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "B"))) ")" )) & (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) ) ")" )) ")" )) ")" ))); theorem :: ORDERS_3:6 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_orders_3 :::"MonFuncs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_orders_3 :::"MonFuncs"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ))) "holds" (Bool (Set (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_orders_3 :::"MonFuncs"::: ) "(" (Set (Var "A")) "," (Set (Var "C")) ")" )))) ; theorem :: ORDERS_3:7 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) ($#r2_hidden :::"in"::: ) (Set ($#k1_orders_3 :::"MonFuncs"::: ) "(" (Set (Var "T")) "," (Set (Var "T")) ")" ))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k1_orders_3 :::"MonFuncs"::: ) "(" "T" "," "T" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"Carr"::: "X" -> ($#m1_hidden :::"set"::: ) means :: ORDERS_3:def 7 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "s")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "st" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "s")))) ")" )) ")" )); end; :: deftheorem defines :::"Carr"::: ORDERS_3:def 7 : (Bool "for" (Set (Var "X")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_orders_3 :::"Carr"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "s")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "st" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "s")))) ")" )) ")" )) ")" )); registrationlet "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"POSet_set":::); cluster (Set ($#k2_orders_3 :::"Carr"::: ) "P") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: ORDERS_3:8 (Bool "for" (Set (Var "f")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool (Set ($#k2_orders_3 :::"Carr"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "f"))) ($#k1_tarski :::"}"::: ) ))) ; theorem :: ORDERS_3:9 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool (Set ($#k2_orders_3 :::"Carr"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "f"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g"))) ($#k2_tarski :::"}"::: ) ))) ; theorem :: ORDERS_3:10 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"POSet_set":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_orders_3 :::"Element"::: ) "of" (Set (Var "P")) "holds" (Bool (Set ($#k1_orders_3 :::"MonFuncs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k1_ens_1 :::"Funcs"::: ) (Set "(" ($#k2_orders_3 :::"Carr"::: ) (Set (Var "P")) ")" ))))) ; theorem :: ORDERS_3:11 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k1_orders_3 :::"MonFuncs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "B"))) ")" ))) ; registrationlet "A", "B" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); cluster (Set ($#k1_orders_3 :::"MonFuncs"::: ) "(" "A" "," "B" ")" ) -> ($#v4_funct_1 :::"functional"::: ) ; end; definitionlet "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"POSet_set":::); func :::"POSCat"::: "P" -> ($#v1_cat_1 :::"strict"::: ) ($#v1_cat_5 :::"with_triple-like_morphisms"::: ) ($#l1_cat_1 :::"Category":::) means :: ORDERS_3:def 8 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) "P") & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_orders_3 :::"Element"::: ) "of" "P" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_ens_1 :::"Funcs"::: ) (Set "(" ($#k2_orders_3 :::"Carr"::: ) "P" ")" )) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_orders_3 :::"MonFuncs"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m1_subset_1 :::"Morphism":::) "of" it)) ")" ) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Morphism":::) "of" it (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_orders_3 :::"Element"::: ) "of" "P"(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_ens_1 :::"Funcs"::: ) (Set "(" ($#k2_orders_3 :::"Carr"::: ) "P" ")" )) "st" (Bool "(" (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_orders_3 :::"MonFuncs"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" it (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_orders_3 :::"Element"::: ) "of" "P" (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_ens_1 :::"Funcs"::: ) (Set "(" ($#k2_orders_3 :::"Carr"::: ) "P" ")" )) "st" (Bool (Bool (Set (Var "m1")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f1")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "m2")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a2")) "," (Set (Var "a3")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "m2")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "m1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a3")) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" (Set (Var "f2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f1")) ")" ) ($#k4_tarski :::"]"::: ) )))) ")" ) ")" ); end; :: deftheorem defines :::"POSCat"::: ORDERS_3:def 8 : (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"POSet_set":::) (Bool "for" (Set (Var "b2")) "being" ($#v1_cat_1 :::"strict"::: ) ($#v1_cat_5 :::"with_triple-like_morphisms"::: ) ($#l1_cat_1 :::"Category":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_orders_3 :::"POSCat"::: ) (Set (Var "P")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_orders_3 :::"Element"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_ens_1 :::"Funcs"::: ) (Set "(" ($#k2_orders_3 :::"Carr"::: ) (Set (Var "P")) ")" )) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_orders_3 :::"MonFuncs"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b2")))) ")" ) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b2")) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_orders_3 :::"Element"::: ) "of" (Set (Var "P"))(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_ens_1 :::"Funcs"::: ) (Set "(" ($#k2_orders_3 :::"Carr"::: ) (Set (Var "P")) ")" )) "st" (Bool "(" (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_orders_3 :::"MonFuncs"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b2")) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_orders_3 :::"Element"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_ens_1 :::"Funcs"::: ) (Set "(" ($#k2_orders_3 :::"Carr"::: ) (Set (Var "P")) ")" )) "st" (Bool (Bool (Set (Var "m1")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f1")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "m2")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a2")) "," (Set (Var "a3")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "m2")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "m1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a3")) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" (Set (Var "f2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f1")) ")" ) ($#k4_tarski :::"]"::: ) )))) ")" ) ")" ) ")" ))); begin scheme :: ORDERS_3:sch 1 AltCatEx{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "C")) "being" ($#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 "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "C"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "C"))) ($#k1_multop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_altcat_1 :::"FuncComp"::: ) "(" (Set F2 "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) "," (Set F2 "(" (Set (Var "j")) "," (Set (Var "k")) ")" ) ")" )) ")" ) ")" ) ")" ) ")" )) provided (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "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 "i")) "," (Set (Var "j")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set F2 "(" (Set (Var "j")) "," (Set (Var "k")) ")" ))) "holds" (Bool (Set (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set F2 "(" (Set (Var "i")) "," (Set (Var "k")) ")" )))) proof end; scheme :: ORDERS_3:sch 2 AltCatUniq{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#v6_altcat_1 :::"strict"::: ) ($#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 "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "C1"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "C1"))) ($#k1_multop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_altcat_1 :::"FuncComp"::: ) "(" (Set F2 "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) "," (Set F2 "(" (Set (Var "j")) "," (Set (Var "k")) ")" ) ")" )) ")" ) ")" ) ")" ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C2"))) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "C2"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "C2"))) ($#k1_multop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_altcat_1 :::"FuncComp"::: ) "(" (Set F2 "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) "," (Set F2 "(" (Set (Var "j")) "," (Set (Var "k")) ")" ) ")" )) ")" ) ")" ) ")" )) "holds" (Bool (Set (Var "C1")) ($#r1_hidden :::"="::: ) (Set (Var "C2")))) proof end; definitionlet "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"POSet_set":::); func :::"POSAltCat"::: "P" -> ($#v6_altcat_1 :::"strict"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) means :: ORDERS_3:def 9 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) "P") & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_orders_3 :::"Element"::: ) "of" "P" "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" it) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_orders_3 :::"MonFuncs"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_orders_3 :::"Element"::: ) "of" "P" "holds" (Bool (Set (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" it) ($#k1_multop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_altcat_1 :::"FuncComp"::: ) "(" (Set "(" ($#k1_orders_3 :::"MonFuncs"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) "," (Set "(" ($#k1_orders_3 :::"MonFuncs"::: ) "(" (Set (Var "j")) "," (Set (Var "k")) ")" ")" ) ")" )) ")" ) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"POSAltCat"::: ORDERS_3:def 9 : (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"POSet_set":::) (Bool "for" (Set (Var "b2")) "being" ($#v6_altcat_1 :::"strict"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_orders_3 :::"POSAltCat"::: ) (Set (Var "P")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_orders_3 :::"Element"::: ) "of" (Set (Var "P")) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "b2"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_orders_3 :::"MonFuncs"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_orders_3 :::"Element"::: ) "of" (Set (Var "P")) "holds" (Bool (Set (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "b2"))) ($#k1_multop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_altcat_1 :::"FuncComp"::: ) "(" (Set "(" ($#k1_orders_3 :::"MonFuncs"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) "," (Set "(" ($#k1_orders_3 :::"MonFuncs"::: ) "(" (Set (Var "j")) "," (Set (Var "k")) ")" ")" ) ")" )) ")" ) ")" ) ")" ) ")" ) ")" ))); registrationlet "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"POSet_set":::); cluster (Set ($#k4_orders_3 :::"POSAltCat"::: ) "P") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v6_altcat_1 :::"strict"::: ) ; end; registrationlet "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"POSet_set":::); cluster (Set ($#k4_orders_3 :::"POSAltCat"::: ) "P") -> ($#v6_altcat_1 :::"strict"::: ) ($#v11_altcat_1 :::"associative"::: ) ($#v12_altcat_1 :::"with_units"::: ) ; end; theorem :: ORDERS_3:12 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"POSet_set":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" ($#k4_orders_3 :::"POSAltCat"::: ) (Set (Var "P")) ")" ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_orders_3 :::"Element"::: ) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "B"))) ")" ))))) ;