:: ORDERS_2 semantic presentation begin definitionattr "c1" is :::"strict"::: ; struct :::"RelStr"::: -> ($#l1_struct_0 :::"1-sorted"::: ) ; aggr :::"RelStr":::(# :::"carrier":::, :::"InternalRel"::: #) -> ($#l1_orders_2 :::"RelStr"::: ) ; sel :::"InternalRel"::: "c1" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")); cluster (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" "X" "," "R" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; definitionlet "A" be ($#l1_orders_2 :::"RelStr"::: ) ; attr "A" is :::"total"::: means :: ORDERS_2:def 1 (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "A") "is" ($#v1_partfun1 :::"total"::: ) ); attr "A" is :::"reflexive"::: means :: ORDERS_2:def 2 (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "A") ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A")); attr "A" is :::"transitive"::: means :: ORDERS_2:def 3 (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "A") ($#r8_relat_2 :::"is_transitive_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A")); attr "A" is :::"antisymmetric"::: means :: ORDERS_2:def 4 (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "A") ($#r4_relat_2 :::"is_antisymmetric_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A")); end; :: deftheorem defines :::"total"::: ORDERS_2:def 1 : (Bool "for" (Set (Var "A")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_orders_2 :::"total"::: ) ) "iff" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A"))) "is" ($#v1_partfun1 :::"total"::: ) ) ")" )); :: deftheorem defines :::"reflexive"::: ORDERS_2:def 2 : (Bool "for" (Set (Var "A")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_orders_2 :::"reflexive"::: ) ) "iff" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A"))) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))) ")" )); :: deftheorem defines :::"transitive"::: ORDERS_2:def 3 : (Bool "for" (Set (Var "A")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_orders_2 :::"transitive"::: ) ) "iff" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A"))) ($#r8_relat_2 :::"is_transitive_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))) ")" )); :: deftheorem defines :::"antisymmetric"::: ORDERS_2:def 4 : (Bool "for" (Set (Var "A")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v5_orders_2 :::"antisymmetric"::: ) ) "iff" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A"))) ($#r4_relat_2 :::"is_antisymmetric_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))) ")" )); registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v1_orders_2 :::"strict"::: ) ($#v2_orders_2 :::"total"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#v3_orders_2 :::"reflexive"::: ) -> ($#v2_orders_2 :::"total"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; definitionmode Poset is ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; end; registrationlet "A" be ($#v2_orders_2 :::"total"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "A") -> ($#v1_partfun1 :::"total"::: ) ; end; registrationlet "A" be ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "A") -> ($#v1_relat_2 :::"reflexive"::: ) ; end; registrationlet "A" be ($#v2_orders_2 :::"total"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "A") -> ($#v4_relat_2 :::"antisymmetric"::: ) ; end; registrationlet "A" be ($#v2_orders_2 :::"total"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "A") -> ($#v8_relat_2 :::"transitive"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "O" be ($#v1_relat_2 :::"reflexive"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")); cluster (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" "X" "," "O" "#)" ) -> ($#v3_orders_2 :::"reflexive"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "O" be ($#v8_relat_2 :::"transitive"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")); cluster (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" "X" "," "O" "#)" ) -> ($#v4_orders_2 :::"transitive"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "O" be ($#v4_relat_2 :::"antisymmetric"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")); cluster (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" "X" "," "O" "#)" ) -> ($#v5_orders_2 :::"antisymmetric"::: ) ; end; definitionlet "A" be ($#l1_orders_2 :::"RelStr"::: ) ; let "a1", "a2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A")); pred "a1" :::"<="::: "a2" means :: ORDERS_2:def 5 (Bool (Set ($#k4_tarski :::"["::: ) "a1" "," "a2" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "A")); end; :: deftheorem defines :::"<="::: ORDERS_2:def 5 : (Bool "for" (Set (Var "A")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a2"))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A")))) ")" ))); notationlet "A" be ($#l1_orders_2 :::"RelStr"::: ) ; let "a1", "a2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A")); synonym "a2" :::">="::: "a1" for "a1" :::"<="::: "a2"; end; definitionlet "A" be ($#l1_orders_2 :::"RelStr"::: ) ; let "a1", "a2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A")); pred "a1" :::"<"::: "a2" means :: ORDERS_2:def 6 (Bool "(" (Bool "a1" ($#r1_orders_2 :::"<="::: ) "a2") & (Bool "a1" ($#r1_hidden :::"<>"::: ) "a2") ")" ); irreflexivity (Bool "for" (Set (Var "a1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A")) "holds" (Bool "(" "not" (Bool (Set (Var "a1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a1"))) "or" "not" (Bool (Set (Var "a1")) ($#r1_hidden :::"<>"::: ) (Set (Var "a1"))) ")" )) ; end; :: deftheorem defines :::"<"::: ORDERS_2:def 6 : (Bool "for" (Set (Var "A")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a2"))) "iff" (Bool "(" (Bool (Set (Var "a1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a2"))) & (Bool (Set (Var "a1")) ($#r1_hidden :::"<>"::: ) (Set (Var "a2"))) ")" ) ")" ))); notationlet "A" be ($#l1_orders_2 :::"RelStr"::: ) ; let "a1", "a2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A")); synonym "a2" :::">"::: "a1" for "a1" :::"<"::: "a2"; end; theorem :: ORDERS_2:1 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a"))))) ; definitionlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "a1", "a2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A")); :: original: :::"<="::: redefine pred "a1" :::"<="::: "a2"; reflexivity (Bool "for" (Set (Var "a1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A")) "holds" (Bool ((Set (Const "A")) "," (Set (Var "b1")) "," (Set (Var "b1"))))) ; end; theorem :: ORDERS_2:2 (Bool "for" (Set (Var "A")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a2"))) & (Bool (Set (Var "a2")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a1")))) "holds" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))))) ; theorem :: ORDERS_2:3 (Bool "for" (Set (Var "A")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a2"))) & (Bool (Set (Var "a2")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a3")))) "holds" (Bool (Set (Var "a1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a3"))))) ; theorem :: ORDERS_2:4 (Bool "for" (Set (Var "A")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool "(" "not" (Bool (Set (Var "a1")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a2"))) "or" "not" (Bool (Set (Var "a2")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a1"))) ")" ))) ; theorem :: ORDERS_2:5 (Bool "for" (Set (Var "A")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a1")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a2"))) & (Bool (Set (Var "a2")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a3")))) "holds" (Bool (Set (Var "a1")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a3"))))) ; theorem :: ORDERS_2:6 (Bool "for" (Set (Var "A")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a2")))) "holds" (Bool "not" (Bool (Set (Var "a2")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a1")))))) ; theorem :: ORDERS_2:7 (Bool "for" (Set (Var "A")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Bool "(" (Bool "(" (Bool (Set (Var "a1")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a2"))) & (Bool (Set (Var "a2")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a3"))) ")" ) "or" (Bool "(" (Bool (Set (Var "a1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a2"))) & (Bool (Set (Var "a2")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a3"))) ")" ) ")" )) "holds" (Bool (Set (Var "a1")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a3"))))) ; definitionlet "A" be ($#l1_orders_2 :::"RelStr"::: ) ; let "IT" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); attr "IT" is :::"strongly_connected"::: means :: ORDERS_2:def 7 (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "A") ($#r7_relat_2 :::"is_strongly_connected_in"::: ) "IT"); end; :: deftheorem defines :::"strongly_connected"::: ORDERS_2:def 7 : (Bool "for" (Set (Var "A")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_orders_2 :::"strongly_connected"::: ) ) "iff" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A"))) ($#r7_relat_2 :::"is_strongly_connected_in"::: ) (Set (Var "IT"))) ")" ))); registrationlet "A" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v6_orders_2 :::"strongly_connected"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A")); end; registrationlet "A" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v6_orders_2 :::"strongly_connected"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A")); end; definitionlet "A" be ($#l1_orders_2 :::"RelStr"::: ) ; mode Chain of "A" is ($#v6_orders_2 :::"strongly_connected"::: ) ($#m1_subset_1 :::"Subset":::) "of" "A"; end; theorem :: ORDERS_2:8 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) "is" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "A"))))) ; theorem :: ORDERS_2:9 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k7_domain_1 :::"}"::: ) ) "is" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Var "a1")) ($#r3_orders_2 :::"<="::: ) (Set (Var "a2"))) "or" (Bool (Set (Var "a2")) ($#r3_orders_2 :::"<="::: ) (Set (Var "a1"))) ")" ) ")" ))) ; theorem :: ORDERS_2:10 (Bool "for" (Set (Var "A")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "S")) "is" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "A")))))) ; theorem :: ORDERS_2:11 (Bool "for" (Set (Var "A")) "being" ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "a1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a2"))) "or" (Bool (Set (Var "a2")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a1"))) ")" ) "iff" (Bool "ex" (Set (Var "C")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) ")" )) ")" ))) ; theorem :: ORDERS_2:12 (Bool "for" (Set (Var "A")) "being" ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool "ex" (Set (Var "C")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) ")" )) "iff" (Bool "(" (Bool (Set (Var "a1")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a2"))) "iff" (Bool (Bool "not" (Set (Var "a2")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a1")))) ")" ) ")" ))) ; theorem :: ORDERS_2:13 (Bool "for" (Set (Var "A")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A"))) ($#r2_wellord1 :::"well_orders"::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "T")) "is" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "A"))))) ; definitionlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); func :::"UpperCone"::: "S" -> ($#m1_subset_1 :::"Subset":::) "of" "A" equals :: ORDERS_2:def 8 "{" (Set (Var "a1")) where a1 "is" ($#m1_subset_1 :::"Element":::) "of" "A" : (Bool "for" (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" "A" "st" (Bool (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) "S")) "holds" (Bool (Set (Var "a2")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a1")))) "}" ; end; :: deftheorem defines :::"UpperCone"::: ORDERS_2:def 8 : (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k1_orders_2 :::"UpperCone"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "a1")) where a1 "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) : (Bool "for" (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "a2")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a1")))) "}" ))); definitionlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); func :::"LowerCone"::: "S" -> ($#m1_subset_1 :::"Subset":::) "of" "A" equals :: ORDERS_2:def 9 "{" (Set (Var "a1")) where a1 "is" ($#m1_subset_1 :::"Element":::) "of" "A" : (Bool "for" (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" "A" "st" (Bool (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) "S")) "holds" (Bool (Set (Var "a1")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a2")))) "}" ; end; :: deftheorem defines :::"LowerCone"::: ORDERS_2:def 9 : (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k2_orders_2 :::"LowerCone"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "a1")) where a1 "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) : (Bool "for" (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "a1")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a2")))) "}" ))); theorem :: ORDERS_2:14 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool (Set ($#k1_orders_2 :::"UpperCone"::: ) (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))))) ; theorem :: ORDERS_2:15 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool (Set ($#k1_orders_2 :::"UpperCone"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: ORDERS_2:16 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool (Set ($#k2_orders_2 :::"LowerCone"::: ) (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))))) ; theorem :: ORDERS_2:17 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool (Set ($#k2_orders_2 :::"LowerCone"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: ORDERS_2:18 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool "not" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_orders_2 :::"UpperCone"::: ) (Set (Var "S")))))))) ; theorem :: ORDERS_2:19 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_orders_2 :::"UpperCone"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: ORDERS_2:20 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool "not" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_orders_2 :::"LowerCone"::: ) (Set (Var "S")))))))) ; theorem :: ORDERS_2:21 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_orders_2 :::"LowerCone"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: ORDERS_2:22 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "c")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a"))) "iff" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_orders_2 :::"UpperCone"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "c")) ($#k6_domain_1 :::"}"::: ) ))) ")" ))) ; theorem :: ORDERS_2:23 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_orders_2 :::"<"::: ) (Set (Var "c"))) "iff" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_orders_2 :::"LowerCone"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "c")) ($#k6_domain_1 :::"}"::: ) ))) ")" ))) ; definitionlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A")); func :::"InitSegm"::: "(" "S" "," "a" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "A" equals :: ORDERS_2:def 10 (Set (Set "(" ($#k2_orders_2 :::"LowerCone"::: ) (Set ($#k6_domain_1 :::"{"::: ) "a" ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k9_subset_1 :::"/\"::: ) "S"); end; :: deftheorem defines :::"InitSegm"::: ORDERS_2:def 10 : (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k3_orders_2 :::"InitSegm"::: ) "(" (Set (Var "S")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_orders_2 :::"LowerCone"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "S"))))))); definitionlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); mode :::"Initial_Segm"::: "of" "S" -> ($#m1_subset_1 :::"Subset":::) "of" "A" means :: ORDERS_2:def 11 (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "A" "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "S") & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_orders_2 :::"InitSegm"::: ) "(" "S" "," (Set (Var "a")) ")" )) ")" )) if (Bool "S" ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"Initial_Segm"::: ORDERS_2:def 11 : (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_orders_2 :::"Initial_Segm"::: ) "of" (Set (Var "S"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_orders_2 :::"InitSegm"::: ) "(" (Set (Var "S")) "," (Set (Var "a")) ")" )) ")" )) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "S")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_orders_2 :::"Initial_Segm"::: ) "of" (Set (Var "S"))) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ")" ))); theorem :: ORDERS_2:24 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k3_orders_2 :::"InitSegm"::: ) "(" (Set (Var "S")) "," (Set (Var "b")) ")" )) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_orders_2 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" ) ")" )))) ; theorem :: ORDERS_2:25 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k3_orders_2 :::"InitSegm"::: ) "(" (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set (Var "A")) ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: ORDERS_2:26 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds" (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k3_orders_2 :::"InitSegm"::: ) "(" (Set (Var "S")) "," (Set (Var "a")) ")" )))))) ; theorem :: ORDERS_2:27 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a1")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a2")))) "holds" (Bool (Set ($#k3_orders_2 :::"InitSegm"::: ) "(" (Set (Var "S")) "," (Set (Var "a1")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_orders_2 :::"InitSegm"::: ) "(" (Set (Var "S")) "," (Set (Var "a2")) ")" ))))) ; theorem :: ORDERS_2:28 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) "holds" (Bool (Set ($#k3_orders_2 :::"InitSegm"::: ) "(" (Set (Var "S")) "," (Set (Var "a")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_orders_2 :::"InitSegm"::: ) "(" (Set (Var "T")) "," (Set (Var "a")) ")" ))))) ; theorem :: ORDERS_2:29 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "I")) "being" ($#m1_orders_2 :::"Initial_Segm"::: ) "of" (Set (Var "S")) "holds" (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "S")))))) ; theorem :: ORDERS_2:30 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool "not" (Bool (Set (Var "S")) "is" ($#m1_orders_2 :::"Initial_Segm"::: ) "of" (Set (Var "S")))) ")" ))) ; theorem :: ORDERS_2:31 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "S")) "is" ($#m1_orders_2 :::"Initial_Segm"::: ) "of" (Set (Var "T")))) "holds" (Bool "not" (Bool (Set (Var "T")) "is" ($#m1_orders_2 :::"Initial_Segm"::: ) "of" (Set (Var "S")))))) ; theorem :: ORDERS_2:32 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a1")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a2"))) & (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Var "T")) "is" ($#m1_orders_2 :::"Initial_Segm"::: ) "of" (Set (Var "S")))) "holds" (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "T")))))) ; theorem :: ORDERS_2:33 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "S")) "is" ($#m1_orders_2 :::"Initial_Segm"::: ) "of" (Set (Var "T")))) "holds" (Bool (Set ($#k3_orders_2 :::"InitSegm"::: ) "(" (Set (Var "S")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_orders_2 :::"InitSegm"::: ) "(" (Set (Var "T")) "," (Set (Var "a")) ")" ))))) ; theorem :: ORDERS_2:34 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set (Var "T"))) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A"))) ($#r2_wellord1 :::"well_orders"::: ) (Set (Var "T"))) & (Bool "(" "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "a1")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a2")))) "holds" (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" ) & (Bool (Bool "not" (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Var "T"))))) "holds" (Bool (Set (Var "S")) "is" ($#m1_orders_2 :::"Initial_Segm"::: ) "of" (Set (Var "T"))))) ; theorem :: ORDERS_2:35 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set (Var "T"))) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A"))) ($#r2_wellord1 :::"well_orders"::: ) (Set (Var "T"))) & (Bool "(" "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Var "a1")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a2")))) "holds" (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" ) & (Bool (Bool "not" (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Var "T"))))) "holds" (Bool (Set (Var "S")) "is" ($#m1_orders_2 :::"Initial_Segm"::: ) "of" (Set (Var "T"))))) ; definitionlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "f" be ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "A")))); mode :::"Chain"::: "of" "f" -> ($#m1_subset_1 :::"Chain":::) "of" "A" means :: ORDERS_2:def 12 (Bool "(" (Bool it ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "A") ($#r2_wellord1 :::"well_orders"::: ) it) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "A" "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_orders_2 :::"UpperCone"::: ) (Set "(" ($#k3_orders_2 :::"InitSegm"::: ) "(" it "," (Set (Var "a")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ) ")" ); end; :: deftheorem defines :::"Chain"::: ORDERS_2:def 12 : (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m2_orders_2 :::"Chain"::: ) "of" (Set (Var "f"))) "iff" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A"))) ($#r2_wellord1 :::"well_orders"::: ) (Set (Var "b3"))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b3")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_orders_2 :::"UpperCone"::: ) (Set "(" ($#k3_orders_2 :::"InitSegm"::: ) "(" (Set (Var "b3")) "," (Set (Var "a")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ) ")" ) ")" )))); theorem :: ORDERS_2:36 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) ")" ) ($#k1_tarski :::"}"::: ) ) "is" ($#m2_orders_2 :::"Chain"::: ) "of" (Set (Var "f"))))) ; theorem :: ORDERS_2:37 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))) (Bool "for" (Set (Var "fC")) "being" ($#m2_orders_2 :::"Chain"::: ) "of" (Set (Var "f")) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))) ($#r2_hidden :::"in"::: ) (Set (Var "fC")))))) ; theorem :: ORDERS_2:38 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))) (Bool "for" (Set (Var "fC")) "being" ($#m2_orders_2 :::"Chain"::: ) "of" (Set (Var "f")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "fC"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))))) "holds" (Bool (Set (Var "b")) ($#r3_orders_2 :::"<="::: ) (Set (Var "a"))))))) ; theorem :: ORDERS_2:39 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))) (Bool "for" (Set (Var "fC")) "being" ($#m2_orders_2 :::"Chain"::: ) "of" (Set (Var "f")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))))) "holds" (Bool (Set ($#k3_orders_2 :::"InitSegm"::: ) "(" (Set (Var "fC")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))))) ; theorem :: ORDERS_2:40 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))) (Bool "for" (Set (Var "fC1")) "," (Set (Var "fC2")) "being" ($#m2_orders_2 :::"Chain"::: ) "of" (Set (Var "f")) "holds" (Bool (Set (Var "fC1")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "fC2")))))) ; theorem :: ORDERS_2:41 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))) (Bool "for" (Set (Var "fC1")) "," (Set (Var "fC2")) "being" ($#m2_orders_2 :::"Chain"::: ) "of" (Set (Var "f")) "st" (Bool (Bool (Set (Var "fC1")) ($#r1_hidden :::"<>"::: ) (Set (Var "fC2")))) "holds" (Bool "(" (Bool (Set (Var "fC1")) "is" ($#m1_orders_2 :::"Initial_Segm"::: ) "of" (Set (Var "fC2"))) "iff" (Bool (Set (Var "fC2")) "is" (Bool "not" ($#m1_orders_2 :::"Initial_Segm"::: ) "of" (Set (Var "fC1")))) ")" )))) ; theorem :: ORDERS_2:42 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))) (Bool "for" (Set (Var "fC1")) "," (Set (Var "fC2")) "being" ($#m2_orders_2 :::"Chain"::: ) "of" (Set (Var "f")) "holds" (Bool "(" (Bool (Set (Var "fC1")) ($#r2_xboole_0 :::"c<"::: ) (Set (Var "fC2"))) "iff" (Bool (Set (Var "fC1")) "is" ($#m1_orders_2 :::"Initial_Segm"::: ) "of" (Set (Var "fC2"))) ")" )))) ; definitionlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "f" be ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "A")))); func :::"Chains"::: "f" -> ($#m1_hidden :::"set"::: ) means :: ORDERS_2:def 13 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#m2_orders_2 :::"Chain"::: ) "of" "f") ")" )); end; :: deftheorem defines :::"Chains"::: ORDERS_2:def 13 : (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_orders_2 :::"Chains"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Var "x")) "is" ($#m2_orders_2 :::"Chain"::: ) "of" (Set (Var "f"))) ")" )) ")" )))); registrationlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "f" be ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "A")))); cluster (Set ($#k4_orders_2 :::"Chains"::: ) "f") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: ORDERS_2:43 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k4_orders_2 :::"Chains"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: ORDERS_2:44 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))) (Bool "for" (Set (Var "fC")) "being" ($#m2_orders_2 :::"Chain"::: ) "of" (Set (Var "f")) "st" (Bool (Bool (Set (Var "fC")) ($#r1_hidden :::"<>"::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k4_orders_2 :::"Chains"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k4_orders_2 :::"Chains"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Var "fC")) "is" ($#m1_orders_2 :::"Initial_Segm"::: ) "of" (Set (Var "S"))))))) ; theorem :: ORDERS_2:45 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k1_orders_1 :::"BOOL"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k4_orders_2 :::"Chains"::: ) (Set (Var "f")) ")" )) "is" ($#m2_orders_2 :::"Chain"::: ) "of" (Set (Var "f"))))) ; begin theorem :: ORDERS_2:46 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A"))) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "S"))))) ; theorem :: ORDERS_2:47 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A"))) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "S"))) "is" ($#v3_orders_1 :::"being_linear-order"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "A"))))) ; theorem :: ORDERS_2:48 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A"))) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "C"))) "is" ($#v3_orders_1 :::"being_linear-order"::: ) ))) ; theorem :: ORDERS_2:49 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A"))) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "S")) "is" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "A"))))) ; theorem :: ORDERS_2:50 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "A")) "holds" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A"))) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "C"))))) ; theorem :: ORDERS_2:51 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r7_orders_1 :::"is_minimal_in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A")))) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool (Bool "not" (Set (Var "b")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a"))))) ")" ))) ; theorem :: ORDERS_2:52 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r6_orders_1 :::"is_maximal_in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A")))) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool (Bool "not" (Set (Var "a")) ($#r2_orders_2 :::"<"::: ) (Set (Var "b"))))) ")" ))) ; theorem :: ORDERS_2:53 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r8_orders_1 :::"is_superior_of"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A")))) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "b")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a")))) ")" ))) ; theorem :: ORDERS_2:54 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r9_orders_1 :::"is_inferior_of"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A")))) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "a")) ($#r2_orders_2 :::"<"::: ) (Set (Var "b")))) ")" ))) ; theorem :: ORDERS_2:55 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) "st" (Bool (Bool "(" "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "A")) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "b")) ($#r3_orders_2 :::"<="::: ) (Set (Var "a"))))) ")" )) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool (Bool "not" (Set (Var "a")) ($#r2_orders_2 :::"<"::: ) (Set (Var "b"))))))) ; theorem :: ORDERS_2:56 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) "st" (Bool (Bool "(" "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "A")) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "a")) ($#r3_orders_2 :::"<="::: ) (Set (Var "b"))))) ")" )) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool (Bool "not" (Set (Var "b")) ($#r2_orders_2 :::"<"::: ) (Set (Var "a"))))))) ; registration cluster ($#v2_struct_0 :::"empty"::: ) ($#v1_orders_2 :::"strict"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end;