:: ORDERS_4  semantic presentation begin  definitionmode  :::"Chain":::  ->    ($#l1_orders_2 :::"RelStr"::: )   means :: ORDERS_4:def 1 (Bool  "("  (Bool it "is"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v16_waybel_0 :::"connected"::: )    ($#l1_orders_2 :::"Poset":::)) "or" (Bool it "is"   ($#v2_struct_0 :::"empty"::: )  )  ")" ); end; 




:: deftheorem    defines :::"Chain"::: ORDERS_4:def 1 :  (Bool  "for" (Set (Var "b1")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b1")) "is"    ($#m1_orders_4 :::"Chain"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "b1")) "is"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v16_waybel_0 :::"connected"::: )    ($#l1_orders_2 :::"Poset":::)) "or" (Bool (Set (Var "b1")) "is"   ($#v2_struct_0 :::"empty"::: )  )  ")" )  ")" )); 
 registration
cluster   ($#v2_struct_0 :::"empty"::: )    ->   ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; registration
cluster   ->   ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )    for    ($#m1_orders_4 :::"Chain"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )  bbbadV2_ORDERS_2()   ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )    for    ($#m1_orders_4 :::"Chain"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v16_waybel_0 :::"connected"::: )    for    ($#m1_orders_4 :::"Chain"::: )  ; 
end; definitionlet "L" be    ($#l1_struct_0 :::"1-sorted"::: )  ; attr "L" is  :::"countable":::  means :: ORDERS_4:def 2 (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "L") "is"   ($#v4_card_3 :::"countable"::: )  ); end; 




:: deftheorem    defines :::"countable"::: ORDERS_4:def 2 :  (Bool  "for" (Set (Var "L")) "being"    ($#l1_struct_0 :::"1-sorted"::: )   "holds"   (Bool  "("  (Bool (Set (Var "L")) "is"   ($#v1_orders_4 :::"countable"::: )  ) "iff" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L"))) "is"   ($#v4_card_3 :::"countable"::: )  )  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_struct_0 :::"finite"::: )   bbbadV2_ORDERS_2()   ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )    for    ($#m1_orders_4 :::"Chain"::: )  ; 
end; registration
cluster bbbadV2_ORDERS_2()   ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_orders_4 :::"countable"::: )    for    ($#m1_orders_4 :::"Chain"::: )  ; 
end; registrationlet "A" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v16_waybel_0 :::"connected"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_yellow_0 :::"full"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v16_waybel_0 :::"connected"::: )    for    ($#m1_yellow_0 :::"SubRelStr"::: )   "of" "A"; 
end; registrationlet "A" be   ($#v8_struct_0 :::"finite"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster   ->   ($#v8_struct_0 :::"finite"::: )    for    ($#m1_yellow_0 :::"SubRelStr"::: )   "of" "A"; 
end; 
theorem :: ORDERS_4:1 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "n"))) "is"   ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "m"))))) ; 
 definitionlet "L" be    ($#l1_orders_2 :::"RelStr"::: )  ; let "A", "B" be    ($#m1_hidden :::"set"::: )  ; pred "A" "," "B" :::"form_upper_lower_partition_of"::: "L" means :: ORDERS_4:def 3 (Bool  "("  (Bool (Set "A"  ($#k2_xboole_0 :::"\/"::: )  "B")  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "L")) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" "L"  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  "A") & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  "B")) "holds"  (Bool (Set (Var "a"))  ($#r2_orders_2 :::"<"::: )  (Set (Var "b")))  ")" )  ")" ); end; 






:: deftheorem    defines :::"form_upper_lower_partition_of"::: ORDERS_4:def 3 :  (Bool  "for" (Set (Var "L")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r1_orders_4 :::"form_upper_lower_partition_of"::: )  (Set (Var "L"))) "iff" (Bool  "("  (Bool (Set (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Var "a"))  ($#r2_orders_2 :::"<"::: )  (Set (Var "b")))  ")" )  ")" )  ")" ))); 
 
theorem :: ORDERS_4:2 (Bool  "for" (Set (Var "L")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r1_orders_4 :::"form_upper_lower_partition_of"::: )  (Set (Var "L")))) "holds"  (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B"))))) ; 
 
theorem :: ORDERS_4:3 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_orders_2 :::"antisymmetric"::: )     ($#v2_yellow_0 :::"upper-bounded"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"  (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  ($#k6_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k4_yellow_0 :::"Top"::: )  (Set (Var "L")) ")" ) ($#k6_domain_1 :::"}"::: ) )) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k4_yellow_0 :::"Top"::: )  (Set (Var "L")) ")" ) ($#k6_domain_1 :::"}"::: ) )  ($#r1_orders_4 :::"form_upper_lower_partition_of"::: )  (Set (Var "L")))) ; 
 
theorem :: ORDERS_4:4 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  )) "holds"  (Bool  "("   "("  (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L1")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")"  &  "("  (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L1")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")"  & (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L1")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" ) &  "("  (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L1")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L2")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")"  &  "("  (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L2")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L1")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")"   ")" ))) ; 
 
theorem :: ORDERS_4:5 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#v5_orders_2 :::"antisymmetric"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A1")) "," (Set (Var "B1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1"))  "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "B1"))  ($#r1_orders_4 :::"form_upper_lower_partition_of"::: )  (Set (Var "L1")))) "holds"  (Bool  "for" (Set (Var "A2")) "," (Set (Var "B2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L2"))  "st" (Bool (Bool (Set (Var "A2")) "," (Set (Var "B2"))  ($#r1_orders_4 :::"form_upper_lower_partition_of"::: )  (Set (Var "L2")))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k5_yellow_0 :::"subrelstr"::: )  (Set (Var "A1")) ")" ) "," (Set  "("  ($#k5_yellow_0 :::"subrelstr"::: )  (Set (Var "A2")) ")" )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  )) "holds"  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k5_yellow_0 :::"subrelstr"::: )  (Set (Var "B1")) ")" ) "," (Set  "("  ($#k5_yellow_0 :::"subrelstr"::: )  (Set (Var "B2")) ")" )  "st" (Bool (Bool (Set (Var "g")) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  )) "holds"  (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2")) "st"  (Bool  "("  (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "g")))) & (Bool (Set (Var "h")) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  )  ")" ))))))) ; 
 
theorem :: ORDERS_4:6 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )     ($#m1_orders_4 :::"Chain"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "A"))))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Var "A")) "," (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "n")))  ($#r5_waybel_1 :::"are_isomorphic"::: )  ))) ;