:: ORDERS_1 semantic presentation begin definitionlet "M" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; assume (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Const "M")))) ; mode :::"Choice_Function"::: "of" "M" -> ($#m1_subset_1 :::"Function":::) "of" "M" "," (Set "(" ($#k3_tarski :::"union"::: ) "M" ")" ) means :: ORDERS_1:def 1 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) "M")) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "X")))); end; :: deftheorem defines :::"Choice_Function"::: ORDERS_1:def 1 : (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "M"))))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "M")) "," (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "M")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set (Var "M"))) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" ))); definitionlet "D" be ($#m1_hidden :::"set"::: ) ; func :::"BOOL"::: "D" -> ($#m1_hidden :::"set"::: ) equals :: ORDERS_1:def 2 (Set (Set "(" ($#k9_setfam_1 :::"bool"::: ) "D" ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )); end; :: deftheorem defines :::"BOOL"::: ORDERS_1:def 2 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_orders_1 :::"BOOL"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "D")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))); registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_orders_1 :::"BOOL"::: ) "D") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: ORDERS_1:1 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_orders_1 :::"BOOL"::: ) (Set (Var "D")))))) ; theorem :: ORDERS_1:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "D")) ($#r2_hidden :::"in"::: ) (Set ($#k1_orders_1 :::"BOOL"::: ) (Set (Var "X")))) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode Order of "X" is ($#v1_relat_2 :::"reflexive"::: ) ($#v4_relat_2 :::"antisymmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_subset_1 :::"Relation":::) "of" "X"; end; theorem :: ORDERS_1:3 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "O"))))) ; theorem :: ORDERS_1:4 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "O"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "O")))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: ORDERS_1:5 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "O"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "O")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "O"))))) ; theorem :: ORDERS_1:6 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "ex" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) "iff" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "Y"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: ORDERS_1:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r7_relat_2 :::"is_strongly_connected_in"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "P")) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "X"))) & (Bool (Set (Var "P")) ($#r6_relat_2 :::"is_connected_in"::: ) (Set (Var "X"))) ")" ) ")" ))) ; theorem :: ORDERS_1:8 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "X"))) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "P")) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "Y"))))) ; theorem :: ORDERS_1:9 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "P")) ($#r4_relat_2 :::"is_antisymmetric_in"::: ) (Set (Var "X"))) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "P")) ($#r4_relat_2 :::"is_antisymmetric_in"::: ) (Set (Var "Y"))))) ; theorem :: ORDERS_1:10 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "P")) ($#r8_relat_2 :::"is_transitive_in"::: ) (Set (Var "X"))) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "P")) ($#r8_relat_2 :::"is_transitive_in"::: ) (Set (Var "Y"))))) ; theorem :: ORDERS_1:11 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "P")) ($#r7_relat_2 :::"is_strongly_connected_in"::: ) (Set (Var "X"))) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "P")) ($#r7_relat_2 :::"is_strongly_connected_in"::: ) (Set (Var "Y"))))) ; theorem :: ORDERS_1:12 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#v1_partfun1 :::"total"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: ORDERS_1:13 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "R")) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" ))) ; begin theorem :: ORDERS_1:14 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "O"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "O"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) ")" ))) ; theorem :: ORDERS_1:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "O"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"being_quasi-order"::: means :: ORDERS_1:def 3 (Bool "(" (Bool "R" "is" ($#v1_relat_2 :::"reflexive"::: ) ) & (Bool "R" "is" ($#v8_relat_2 :::"transitive"::: ) ) ")" ); attr "R" is :::"being_partial-order"::: means :: ORDERS_1:def 4 (Bool "(" (Bool "R" "is" ($#v1_relat_2 :::"reflexive"::: ) ) & (Bool "R" "is" ($#v8_relat_2 :::"transitive"::: ) ) & (Bool "R" "is" ($#v4_relat_2 :::"antisymmetric"::: ) ) ")" ); attr "R" is :::"being_linear-order"::: means :: ORDERS_1:def 5 (Bool "(" (Bool "R" "is" ($#v1_relat_2 :::"reflexive"::: ) ) & (Bool "R" "is" ($#v8_relat_2 :::"transitive"::: ) ) & (Bool "R" "is" ($#v4_relat_2 :::"antisymmetric"::: ) ) & (Bool "R" "is" ($#v6_relat_2 :::"connected"::: ) ) ")" ); end; :: deftheorem defines :::"being_quasi-order"::: ORDERS_1:def 3 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_orders_1 :::"being_quasi-order"::: ) ) "iff" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_relat_2 :::"reflexive"::: ) ) & (Bool (Set (Var "R")) "is" ($#v8_relat_2 :::"transitive"::: ) ) ")" ) ")" )); :: deftheorem defines :::"being_partial-order"::: ORDERS_1:def 4 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v2_orders_1 :::"being_partial-order"::: ) ) "iff" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_relat_2 :::"reflexive"::: ) ) & (Bool (Set (Var "R")) "is" ($#v8_relat_2 :::"transitive"::: ) ) & (Bool (Set (Var "R")) "is" ($#v4_relat_2 :::"antisymmetric"::: ) ) ")" ) ")" )); :: deftheorem defines :::"being_linear-order"::: ORDERS_1:def 5 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v3_orders_1 :::"being_linear-order"::: ) ) "iff" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_relat_2 :::"reflexive"::: ) ) & (Bool (Set (Var "R")) "is" ($#v8_relat_2 :::"transitive"::: ) ) & (Bool (Set (Var "R")) "is" ($#v4_relat_2 :::"antisymmetric"::: ) ) & (Bool (Set (Var "R")) "is" ($#v6_relat_2 :::"connected"::: ) ) ")" ) ")" )); theorem :: ORDERS_1:16 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) "is" ($#v1_orders_1 :::"being_quasi-order"::: ) )) "holds" (Bool (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ) "is" ($#v1_orders_1 :::"being_quasi-order"::: ) )) ; theorem :: ORDERS_1:17 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) "is" ($#v2_orders_1 :::"being_partial-order"::: ) )) "holds" (Bool (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ) "is" ($#v2_orders_1 :::"being_partial-order"::: ) )) ; theorem :: ORDERS_1:18 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_orders_1 :::"being_linear-order"::: ) )) "holds" (Bool (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ) "is" ($#v3_orders_1 :::"being_linear-order"::: ) )) ; theorem :: ORDERS_1:19 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) "is" ($#v2_wellord1 :::"well-ordering"::: ) )) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_orders_1 :::"being_quasi-order"::: ) ) & (Bool (Set (Var "R")) "is" ($#v2_orders_1 :::"being_partial-order"::: ) ) & (Bool (Set (Var "R")) "is" ($#v3_orders_1 :::"being_linear-order"::: ) ) ")" )) ; theorem :: ORDERS_1:20 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_orders_1 :::"being_linear-order"::: ) )) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_orders_1 :::"being_quasi-order"::: ) ) & (Bool (Set (Var "R")) "is" ($#v2_orders_1 :::"being_partial-order"::: ) ) ")" )) ; theorem :: ORDERS_1:21 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) "is" ($#v2_orders_1 :::"being_partial-order"::: ) )) "holds" (Bool (Set (Var "R")) "is" ($#v1_orders_1 :::"being_quasi-order"::: ) )) ; theorem :: ORDERS_1:22 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "O")) "is" ($#v2_orders_1 :::"being_partial-order"::: ) ))) ; theorem :: ORDERS_1:23 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "O")) "is" ($#v1_orders_1 :::"being_quasi-order"::: ) ))) ; theorem :: ORDERS_1:24 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "O")) "is" ($#v6_relat_2 :::"connected"::: ) )) "holds" (Bool (Set (Var "O")) "is" ($#v3_orders_1 :::"being_linear-order"::: ) ))) ; theorem :: ORDERS_1:25 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v1_orders_1 :::"being_quasi-order"::: ) )) "holds" (Bool (Set (Set (Var "R")) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "X"))) "is" ($#v1_orders_1 :::"being_quasi-order"::: ) ))) ; theorem :: ORDERS_1:26 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v2_orders_1 :::"being_partial-order"::: ) )) "holds" (Bool (Set (Set (Var "R")) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "X"))) "is" ($#v2_orders_1 :::"being_partial-order"::: ) ))) ; theorem :: ORDERS_1:27 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_orders_1 :::"being_linear-order"::: ) )) "holds" (Bool (Set (Set (Var "R")) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "X"))) "is" ($#v3_orders_1 :::"being_linear-order"::: ) ))) ; registrationlet "R" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k1_relat_1 :::"field"::: ) "R") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registration cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) -> ($#v2_wellord1 :::"well-ordering"::: ) ($#v1_orders_1 :::"being_quasi-order"::: ) ($#v2_orders_1 :::"being_partial-order"::: ) ($#v3_orders_1 :::"being_linear-order"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_relat_1 :::"id"::: ) "X") -> ($#v1_orders_1 :::"being_quasi-order"::: ) ($#v2_orders_1 :::"being_partial-order"::: ) ; end; definitionlet "R" be ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; pred "R" :::"quasi_orders"::: "X" means :: ORDERS_1:def 6 (Bool "(" (Bool "R" ($#r1_relat_2 :::"is_reflexive_in"::: ) "X") & (Bool "R" ($#r8_relat_2 :::"is_transitive_in"::: ) "X") ")" ); pred "R" :::"partially_orders"::: "X" means :: ORDERS_1:def 7 (Bool "(" (Bool "R" ($#r1_relat_2 :::"is_reflexive_in"::: ) "X") & (Bool "R" ($#r8_relat_2 :::"is_transitive_in"::: ) "X") & (Bool "R" ($#r4_relat_2 :::"is_antisymmetric_in"::: ) "X") ")" ); pred "R" :::"linearly_orders"::: "X" means :: ORDERS_1:def 8 (Bool "(" (Bool "R" ($#r1_relat_2 :::"is_reflexive_in"::: ) "X") & (Bool "R" ($#r8_relat_2 :::"is_transitive_in"::: ) "X") & (Bool "R" ($#r4_relat_2 :::"is_antisymmetric_in"::: ) "X") & (Bool "R" ($#r6_relat_2 :::"is_connected_in"::: ) "X") ")" ); end; :: deftheorem defines :::"quasi_orders"::: ORDERS_1:def 6 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "R")) ($#r1_orders_1 :::"quasi_orders"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "R")) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "X"))) & (Bool (Set (Var "R")) ($#r8_relat_2 :::"is_transitive_in"::: ) (Set (Var "X"))) ")" ) ")" ))); :: deftheorem defines :::"partially_orders"::: ORDERS_1:def 7 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "R")) ($#r2_orders_1 :::"partially_orders"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "R")) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "X"))) & (Bool (Set (Var "R")) ($#r8_relat_2 :::"is_transitive_in"::: ) (Set (Var "X"))) & (Bool (Set (Var "R")) ($#r4_relat_2 :::"is_antisymmetric_in"::: ) (Set (Var "X"))) ")" ) ")" ))); :: deftheorem defines :::"linearly_orders"::: ORDERS_1:def 8 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "R")) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "X"))) & (Bool (Set (Var "R")) ($#r8_relat_2 :::"is_transitive_in"::: ) (Set (Var "X"))) & (Bool (Set (Var "R")) ($#r4_relat_2 :::"is_antisymmetric_in"::: ) (Set (Var "X"))) & (Bool (Set (Var "R")) ($#r6_relat_2 :::"is_connected_in"::: ) (Set (Var "X"))) ")" ) ")" ))); theorem :: ORDERS_1:28 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r2_wellord1 :::"well_orders"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Var "R")) ($#r1_orders_1 :::"quasi_orders"::: ) (Set (Var "X"))) & (Bool (Set (Var "R")) ($#r2_orders_1 :::"partially_orders"::: ) (Set (Var "X"))) & (Bool (Set (Var "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "X"))) ")" ))) ; theorem :: ORDERS_1:29 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Var "R")) ($#r1_orders_1 :::"quasi_orders"::: ) (Set (Var "X"))) & (Bool (Set (Var "R")) ($#r2_orders_1 :::"partially_orders"::: ) (Set (Var "X"))) ")" ))) ; theorem :: ORDERS_1:30 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r2_orders_1 :::"partially_orders"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "R")) ($#r1_orders_1 :::"quasi_orders"::: ) (Set (Var "X"))))) ; theorem :: ORDERS_1:31 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) "is" ($#v1_orders_1 :::"being_quasi-order"::: ) )) "holds" (Bool (Set (Var "R")) ($#r1_orders_1 :::"quasi_orders"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R"))))) ; theorem :: ORDERS_1:32 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r1_orders_1 :::"quasi_orders"::: ) (Set (Var "Y"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "R")) ($#r1_orders_1 :::"quasi_orders"::: ) (Set (Var "X"))))) ; theorem :: ORDERS_1:33 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r1_orders_1 :::"quasi_orders"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "X"))) "is" ($#v1_orders_1 :::"being_quasi-order"::: ) ))) ; theorem :: ORDERS_1:34 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) "is" ($#v2_orders_1 :::"being_partial-order"::: ) )) "holds" (Bool (Set (Var "R")) ($#r2_orders_1 :::"partially_orders"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R"))))) ; theorem :: ORDERS_1:35 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r2_orders_1 :::"partially_orders"::: ) (Set (Var "Y"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "R")) ($#r2_orders_1 :::"partially_orders"::: ) (Set (Var "X"))))) ; theorem :: ORDERS_1:36 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r2_orders_1 :::"partially_orders"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "X"))) "is" ($#v2_orders_1 :::"being_partial-order"::: ) ))) ; theorem :: ORDERS_1:37 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_orders_1 :::"being_linear-order"::: ) )) "holds" (Bool (Set (Var "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R"))))) ; theorem :: ORDERS_1:38 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "Y"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "X"))))) ; theorem :: ORDERS_1:39 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "X"))) "is" ($#v3_orders_1 :::"being_linear-order"::: ) ))) ; theorem :: ORDERS_1:40 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r1_orders_1 :::"quasi_orders"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ) ($#r1_orders_1 :::"quasi_orders"::: ) (Set (Var "X"))))) ; theorem :: ORDERS_1:41 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r2_orders_1 :::"partially_orders"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ) ($#r2_orders_1 :::"partially_orders"::: ) (Set (Var "X"))))) ; theorem :: ORDERS_1:42 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "X"))))) ; theorem :: ORDERS_1:43 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "O")) ($#r1_orders_1 :::"quasi_orders"::: ) (Set (Var "X"))))) ; theorem :: ORDERS_1:44 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "O")) ($#r2_orders_1 :::"partially_orders"::: ) (Set (Var "X"))))) ; theorem :: ORDERS_1:45 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r2_orders_1 :::"partially_orders"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "X"))) "is" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X"))))) ; theorem :: ORDERS_1:46 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "X"))) "is" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X"))))) ; theorem :: ORDERS_1:47 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r2_wellord1 :::"well_orders"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "X"))) "is" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X"))))) ; theorem :: ORDERS_1:48 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X"))) ($#r1_orders_1 :::"quasi_orders"::: ) (Set (Var "X"))) & (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X"))) ($#r2_orders_1 :::"partially_orders"::: ) (Set (Var "X"))) ")" )) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; pred "X" :::"has_upper_Zorn_property_wrt"::: "R" means :: ORDERS_1:def 9 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) "X") & (Bool (Set "R" ($#k2_wellord1 :::"|_2"::: ) (Set (Var "Y"))) "is" ($#v3_orders_1 :::"being_linear-order"::: ) )) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X") & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" ) ")" ))); pred "X" :::"has_lower_Zorn_property_wrt"::: "R" means :: ORDERS_1:def 10 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) "X") & (Bool (Set "R" ($#k2_wellord1 :::"|_2"::: ) (Set (Var "Y"))) "is" ($#v3_orders_1 :::"being_linear-order"::: ) )) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X") & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" ) ")" ))); end; :: deftheorem defines :::"has_upper_Zorn_property_wrt"::: ORDERS_1:def 9 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r4_orders_1 :::"has_upper_Zorn_property_wrt"::: ) (Set (Var "R"))) "iff" (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "R")) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "Y"))) "is" ($#v3_orders_1 :::"being_linear-order"::: ) )) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" ))) ")" ))); :: deftheorem defines :::"has_lower_Zorn_property_wrt"::: ORDERS_1:def 10 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r5_orders_1 :::"has_lower_Zorn_property_wrt"::: ) (Set (Var "R"))) "iff" (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "R")) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "Y"))) "is" ($#v3_orders_1 :::"being_linear-order"::: ) )) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" ))) ")" ))); theorem :: ORDERS_1:49 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r4_orders_1 :::"has_upper_Zorn_property_wrt"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: ORDERS_1:50 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r5_orders_1 :::"has_lower_Zorn_property_wrt"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: ORDERS_1:51 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r4_orders_1 :::"has_upper_Zorn_property_wrt"::: ) (Set (Var "R"))) "iff" (Bool (Set (Var "X")) ($#r5_orders_1 :::"has_lower_Zorn_property_wrt"::: ) (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) )) ")" ))) ; theorem :: ORDERS_1:52 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r4_orders_1 :::"has_upper_Zorn_property_wrt"::: ) (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) )) "iff" (Bool (Set (Var "X")) ($#r5_orders_1 :::"has_lower_Zorn_property_wrt"::: ) (Set (Var "R"))) ")" ))) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); let "x" be ($#m1_hidden :::"set"::: ) ; pred "x" :::"is_maximal_in"::: "R" means :: ORDERS_1:def 11 (Bool "(" (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) "R")) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) "R")) "or" "not" (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) "x") "or" "not" (Bool (Set ($#k4_tarski :::"["::: ) "x" "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" ) ")" ) ")" ); pred "x" :::"is_minimal_in"::: "R" means :: ORDERS_1:def 12 (Bool "(" (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) "R")) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) "R")) "or" "not" (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) "x") "or" "not" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," "x" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" ) ")" ) ")" ); pred "x" :::"is_superior_of"::: "R" means :: ORDERS_1:def 13 (Bool "(" (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) "R")) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) "R")) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) "x")) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," "x" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" ) ")" ); pred "x" :::"is_inferior_of"::: "R" means :: ORDERS_1:def 14 (Bool "(" (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) "R")) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) "R")) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) "x")) "holds" (Bool (Set ($#k4_tarski :::"["::: ) "x" "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" ) ")" ); end; :: deftheorem defines :::"is_maximal_in"::: ORDERS_1:def 11 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r6_orders_1 :::"is_maximal_in"::: ) (Set (Var "R"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))) "or" "not" (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) "or" "not" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" ) ")" ) ")" ))); :: deftheorem defines :::"is_minimal_in"::: ORDERS_1:def 12 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r7_orders_1 :::"is_minimal_in"::: ) (Set (Var "R"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))) "or" "not" (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) "or" "not" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" ) ")" ) ")" ))); :: deftheorem defines :::"is_superior_of"::: ORDERS_1:def 13 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r8_orders_1 :::"is_superior_of"::: ) (Set (Var "R"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))) & (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")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "x")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" ) ")" ))); :: deftheorem defines :::"is_inferior_of"::: ORDERS_1:def 14 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r9_orders_1 :::"is_inferior_of"::: ) (Set (Var "R"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))) & (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")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "x")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" ) ")" ))); theorem :: ORDERS_1:53 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r9_orders_1 :::"is_inferior_of"::: ) (Set (Var "R"))) & (Bool (Set (Var "R")) "is" ($#v4_relat_2 :::"antisymmetric"::: ) )) "holds" (Bool (Set (Var "x")) ($#r7_orders_1 :::"is_minimal_in"::: ) (Set (Var "R"))))) ; theorem :: ORDERS_1:54 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r8_orders_1 :::"is_superior_of"::: ) (Set (Var "R"))) & (Bool (Set (Var "R")) "is" ($#v4_relat_2 :::"antisymmetric"::: ) )) "holds" (Bool (Set (Var "x")) ($#r6_orders_1 :::"is_maximal_in"::: ) (Set (Var "R"))))) ; theorem :: ORDERS_1:55 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r7_orders_1 :::"is_minimal_in"::: ) (Set (Var "R"))) & (Bool (Set (Var "R")) "is" ($#v6_relat_2 :::"connected"::: ) )) "holds" (Bool (Set (Var "x")) ($#r9_orders_1 :::"is_inferior_of"::: ) (Set (Var "R"))))) ; theorem :: ORDERS_1:56 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r6_orders_1 :::"is_maximal_in"::: ) (Set (Var "R"))) & (Bool (Set (Var "R")) "is" ($#v6_relat_2 :::"connected"::: ) )) "holds" (Bool (Set (Var "x")) ($#r8_orders_1 :::"is_superior_of"::: ) (Set (Var "R"))))) ; theorem :: ORDERS_1:57 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r8_orders_1 :::"is_superior_of"::: ) (Set (Var "R"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))) & (Bool (Set (Var "R")) "is" ($#v1_relat_2 :::"reflexive"::: ) )) "holds" (Bool (Set (Var "X")) ($#r4_orders_1 :::"has_upper_Zorn_property_wrt"::: ) (Set (Var "R"))))) ; theorem :: ORDERS_1:58 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r9_orders_1 :::"is_inferior_of"::: ) (Set (Var "R"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))) & (Bool (Set (Var "R")) "is" ($#v1_relat_2 :::"reflexive"::: ) )) "holds" (Bool (Set (Var "X")) ($#r5_orders_1 :::"has_lower_Zorn_property_wrt"::: ) (Set (Var "R"))))) ; theorem :: ORDERS_1:59 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r7_orders_1 :::"is_minimal_in"::: ) (Set (Var "R"))) "iff" (Bool (Set (Var "x")) ($#r6_orders_1 :::"is_maximal_in"::: ) (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) )) ")" ))) ; theorem :: ORDERS_1:60 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r7_orders_1 :::"is_minimal_in"::: ) (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) )) "iff" (Bool (Set (Var "x")) ($#r6_orders_1 :::"is_maximal_in"::: ) (Set (Var "R"))) ")" ))) ; theorem :: ORDERS_1:61 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r9_orders_1 :::"is_inferior_of"::: ) (Set (Var "R"))) "iff" (Bool (Set (Var "x")) ($#r8_orders_1 :::"is_superior_of"::: ) (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) )) ")" ))) ; theorem :: ORDERS_1:62 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r9_orders_1 :::"is_inferior_of"::: ) (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) )) "iff" (Bool (Set (Var "x")) ($#r8_orders_1 :::"is_superior_of"::: ) (Set (Var "R"))) ")" ))) ; theorem :: ORDERS_1:63 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r2_orders_1 :::"partially_orders"::: ) (Set (Var "X"))) & (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) ($#r4_orders_1 :::"has_upper_Zorn_property_wrt"::: ) (Set (Var "R")))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r6_orders_1 :::"is_maximal_in"::: ) (Set (Var "R")))))) ; theorem :: ORDERS_1:64 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r2_orders_1 :::"partially_orders"::: ) (Set (Var "X"))) & (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) ($#r5_orders_1 :::"has_lower_Zorn_property_wrt"::: ) (Set (Var "R")))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r7_orders_1 :::"is_minimal_in"::: ) (Set (Var "R")))))) ; theorem :: ORDERS_1:65 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "Z")) "is" ($#v6_ordinal1 :::"c=-linear"::: ) )) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "X1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X1")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "X1")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ) ")" )) ")" )) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "Z")) ($#r1_hidden :::"<>"::: ) (Set (Var "Y")))) "holds" (Bool "not" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "Z")))) ")" ) ")" ))) ; theorem :: ORDERS_1:66 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "Z")) "is" ($#v6_ordinal1 :::"c=-linear"::: ) )) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "X1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X1")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X1"))) ")" ) ")" )) ")" )) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "Z")) ($#r1_hidden :::"<>"::: ) (Set (Var "Y")))) "holds" (Bool "not" (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) ")" ) ")" ))) ; theorem :: ORDERS_1:67 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "Z")) "is" ($#v6_ordinal1 :::"c=-linear"::: ) )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "Z"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "Z")) ($#r1_hidden :::"<>"::: ) (Set (Var "Y")))) "holds" (Bool "not" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "Z")))) ")" ) ")" ))) ; theorem :: ORDERS_1:68 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "Z")) "is" ($#v6_ordinal1 :::"c=-linear"::: ) )) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "Z"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "Z")) ($#r1_hidden :::"<>"::: ) (Set (Var "Y")))) "holds" (Bool "not" (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) ")" ) ")" ))) ; scheme :: ORDERS_1:sch 1 ZornMax{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool "not" (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])))) provided (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool P1[(Set (Var "x")) "," (Set (Var "x"))])) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) & (Bool P1[(Set (Var "y")) "," (Set (Var "x"))])) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) & (Bool P1[(Set (Var "y")) "," (Set (Var "z"))])) "holds" (Bool P1[(Set (Var "x")) "," (Set (Var "z"))])) and (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set F1 "(" ")" )) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])) "holds" (Bool P1[(Set (Var "y")) "," (Set (Var "x"))]) ")" )) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])))) proof end; scheme :: ORDERS_1:sch 2 ZornMin{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool "not" (Bool P1[(Set (Var "y")) "," (Set (Var "x"))])))) provided (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool P1[(Set (Var "x")) "," (Set (Var "x"))])) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) & (Bool P1[(Set (Var "y")) "," (Set (Var "x"))])) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) & (Bool P1[(Set (Var "y")) "," (Set (Var "z"))])) "holds" (Bool P1[(Set (Var "x")) "," (Set (Var "z"))])) and (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set F1 "(" ")" )) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])) "holds" (Bool P1[(Set (Var "y")) "," (Set (Var "x"))]) ")" )) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool P1[(Set (Var "y")) "," (Set (Var "x"))])))) proof end; theorem :: ORDERS_1:69 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r2_orders_1 :::"partially_orders"::: ) (Set (Var "X"))) & (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool "(" (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "P")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "X"))) & (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) ")" )))) ; theorem :: ORDERS_1:70 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_relat_1 :::"field"::: ) (Set (Var "R")) ")" ) "," (Set "(" ($#k1_relat_1 :::"field"::: ) (Set (Var "R")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) ; theorem :: ORDERS_1:71 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v1_relat_2 :::"reflexive"::: ) ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set "(" (Set (Var "R")) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: ORDERS_1:72 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "X"))) "is" ($#v1_relat_2 :::"reflexive"::: ) ))) ; theorem :: ORDERS_1:73 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r8_relat_2 :::"is_transitive_in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "X"))) "is" ($#v8_relat_2 :::"transitive"::: ) ))) ; theorem :: ORDERS_1:74 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r4_relat_2 :::"is_antisymmetric_in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "X"))) "is" ($#v4_relat_2 :::"antisymmetric"::: ) ))) ; theorem :: ORDERS_1:75 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r6_relat_2 :::"is_connected_in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "X"))) "is" ($#v6_relat_2 :::"connected"::: ) ))) ; theorem :: ORDERS_1:76 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r6_relat_2 :::"is_connected_in"::: ) (Set (Var "X"))) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "R")) ($#r6_relat_2 :::"is_connected_in"::: ) (Set (Var "Y"))))) ; theorem :: ORDERS_1:77 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r2_wellord1 :::"well_orders"::: ) (Set (Var "X"))) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "R")) ($#r2_wellord1 :::"well_orders"::: ) (Set (Var "Y"))))) ; theorem :: ORDERS_1:78 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) "is" ($#v6_relat_2 :::"connected"::: ) )) "holds" (Bool (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ) "is" ($#v6_relat_2 :::"connected"::: ) )) ; theorem :: ORDERS_1:79 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "X"))))) ; theorem :: ORDERS_1:80 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r8_relat_2 :::"is_transitive_in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ) ($#r8_relat_2 :::"is_transitive_in"::: ) (Set (Var "X"))))) ; theorem :: ORDERS_1:81 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r4_relat_2 :::"is_antisymmetric_in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ) ($#r4_relat_2 :::"is_antisymmetric_in"::: ) (Set (Var "X"))))) ; theorem :: ORDERS_1:82 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r6_relat_2 :::"is_connected_in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ) ($#r6_relat_2 :::"is_connected_in"::: ) (Set (Var "X"))))) ; theorem :: ORDERS_1:83 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "X")) ")" ) ($#k2_relat_1 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "X")))))) ; theorem :: ORDERS_1:84 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k2_wellord1 :::"|_2"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; begin theorem :: ORDERS_1:85 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "Y")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Var "Z"))) ")" )))) ; theorem :: ORDERS_1:86 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R"))) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set (Var "R")) "is" ($#v1_finset_1 :::"finite"::: ) )) ; theorem :: ORDERS_1:87 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set (Var "R")) "is" ($#v1_finset_1 :::"finite"::: ) )) ; registration cluster (Set ($#k2_wellord2 :::"order_type_of"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: ORDERS_1:88 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k2_wellord2 :::"order_type_of"::: ) (Set "(" ($#k1_wellord2 :::"RelIncl"::: ) (Set (Var "O")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "O")))) ;