:: ARROW  semantic presentation begin  definitionlet "A", "B9" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "B" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "B9")); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set (Const "B")); let "x" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "A")); :: original: :::"."::: redefine func "f" :::"."::: "x" ->    ($#m2_subset_1 :::"Element"::: )   "of" "B"; end; 
theorem :: ARROW:1 (Bool  "for" (Set (Var "A")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A")) (Bool  "ex" (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A")) "st" (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a")))))) ; 
 
theorem :: ARROW:2 (Bool  "for" (Set (Var "A")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">="::: )  (Num 3))) "holds"  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A")) (Bool  "ex" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A")) "st"  (Bool  "("  (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))  ")" )))) ; 
 begin  










definitionlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; func  :::"LinPreorders"::: "A" ->    ($#m1_hidden :::"set"::: )   means :: ARROW:def 1 (Bool  "for" (Set (Var "R")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool (Set (Var "R")) "is"   ($#m1_subset_1 :::"Relation":::) "of" "A") & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "A"  "holds"  (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))) "or" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "A"  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))  ")" )  ")" )  ")" )); end; 





:: deftheorem    defines :::"LinPreorders"::: ARROW:def 1 :  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A")))) "iff" (Bool  "for" (Set (Var "R")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool  "("  (Bool (Set (Var "R")) "is"   ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A"))) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "holds"  (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))) "or" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))  ")" )  ")" )  ")" ))  ")" ))); 
 registrationlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k2_arrow :::"LinPreorders"::: )  "A") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; definitionlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; func  :::"LinOrders"::: "A" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_arrow :::"LinPreorders"::: )  "A" ")" ) means :: ARROW:def 2 (Bool  "for" (Set (Var "R")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arrow :::"LinPreorders"::: )  "A") "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "A"  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))  ")" )); end; 





:: deftheorem    defines :::"LinOrders"::: ARROW:def 2 :  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_arrow :::"LinOrders"::: )  (Set (Var "A")))) "iff" (Bool  "for" (Set (Var "R")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A"))) "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))  ")" ))  ")" ))); 
 registrationlet "A" be    ($#m1_hidden :::"set"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   "A"  ($#v4_relat_1 :::"-defined"::: )   "A"  ($#v5_relat_1 :::"-valued"::: )   bbbadV1_PARTFUN1("A")   ($#v1_relat_2 :::"reflexive"::: )     ($#v4_relat_2 :::"antisymmetric"::: )     ($#v6_relat_2 :::"connected"::: )     ($#v8_relat_2 :::"transitive"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "A" ($#k2_zfmisc_1 :::":]"::: ) )); 
end; definitionlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; redefine func  :::"LinOrders"::: "A" means :: ARROW:def 3 (Bool  "for" (Set (Var "R")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "R")) "is"   ($#v6_relat_2 :::"connected"::: )    ($#m1_subset_1 :::"Order":::) "of" "A")  ")" )); end; 





:: deftheorem    defines :::"LinOrders"::: ARROW:def 3 :  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_arrow :::"LinOrders"::: )  (Set (Var "A")))) "iff" (Bool  "for" (Set (Var "R")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool (Set (Var "R")) "is"   ($#v6_relat_2 :::"connected"::: )    ($#m1_subset_1 :::"Order":::) "of" (Set (Var "A")))  ")" ))  ")" ))); 
 registrationlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k3_arrow :::"LinOrders"::: )  "A") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; registrationlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster   ->   ($#v1_relat_1 :::"Relation-like"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arrow :::"LinPreorders"::: )  "A"); 

cluster   ->   ($#v1_relat_1 :::"Relation-like"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_arrow :::"LinOrders"::: )  "A"); 
end; 






definitionlet "o" be   ($#m1_hidden :::"Relation":::); let "a", "b" be    ($#m1_hidden :::"set"::: )  ; pred "a" :::"<=_"::: "o" "," "b" means :: ARROW:def 4 (Bool (Set  ($#k4_tarski :::"["::: ) "a" "," "b" ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "o"); end; 






:: deftheorem    defines :::"<=_"::: ARROW:def 4 :  (Bool  "for" (Set (Var "o")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r1_arrow :::"<=_"::: )  (Set (Var "o")) "," (Set (Var "b"))) "iff" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "o")))  ")" ))); 
 notationlet "o" be   ($#m1_hidden :::"Relation":::); let "a", "b" be    ($#m1_hidden :::"set"::: )  ; synonym "b" :::">=_"::: "o" "," "a" for "a" :::"<=_"::: "o" "," "b"; antonym "b" :::"<_"::: "o" "," "a" for "a" :::"<=_"::: "o" "," "b"; antonym "a" :::">_"::: "o" "," "b" for "a" :::"<=_"::: "o" "," "b"; end; 
theorem :: ARROW:3 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "o")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Var "a"))  ($#r1_arrow :::"<=_"::: )  (Set (Var "o")) "," (Set (Var "a")))))) ; 
 
theorem :: ARROW:4 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "o")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A")))  "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_arrow :::"<=_"::: )  (Set (Var "o")) "," (Set (Var "b"))) "or" (Bool (Set (Var "b"))  ($#r1_arrow :::"<=_"::: )  (Set (Var "o")) "," (Set (Var "a")))  ")" )))) ; 
 
theorem :: ARROW:5 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "o")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A")))  "st" (Bool (Bool  "("  (Bool (Set (Var "a"))  ($#r1_arrow :::"<=_"::: )  (Set (Var "o")) "," (Set (Var "b"))) "or" (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "b")))  ")" ) & (Bool  "("  (Bool (Set (Var "b"))  ($#r1_arrow :::"<=_"::: )  (Set (Var "o")) "," (Set (Var "c"))) "or" (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "c")))  ")" )) "holds"  (Bool (Set (Var "a"))  ($#r1_arrow :::"<=_"::: )  (Set (Var "o")) "," (Set (Var "c")))))) ; 
 
theorem :: ARROW:6 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "o99")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_arrow :::"LinOrders"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_arrow :::"<=_"::: )  (Set (Var "o99")) "," (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_arrow :::"<=_"::: )  (Set (Var "o99")) "," (Set (Var "a")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))))) ; 
 
theorem :: ARROW:7 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c")))) "holds"  (Bool  "ex" (Set (Var "o")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A"))) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "c")))  ")" )))) ; 
 
theorem :: ARROW:8 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A")) (Bool  "ex" (Set (Var "o")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A"))) "st"  (Bool  "for" (Set (Var "a")) "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"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "a"))))))) ; 
 
theorem :: ARROW:9 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A")) (Bool  "ex" (Set (Var "o")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A"))) "st"  (Bool  "for" (Set (Var "a")) "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"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "b"))))))) ; 
 
theorem :: ARROW:10 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "o9")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c")))) "holds"  (Bool  "ex" (Set (Var "o")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A"))) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "c"))) &  "("  (Bool (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "c")))) "implies" (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "c")))  ")"  &  "("  (Bool (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "c")))) "implies" (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "c")))  ")"  &  "("  (Bool (Bool (Set (Var "c"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "b")))) "implies" (Bool (Set (Var "c"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "b")))  ")"  &  "("  (Bool (Bool (Set (Var "c"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "b")))) "implies" (Bool (Set (Var "c"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "b")))  ")"   ")" ))))) ; 
 
theorem :: ARROW:11 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "o9")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c")))) "holds"  (Bool  "ex" (Set (Var "o")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A"))) "st"  (Bool  "("  (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "a"))) & (Bool (Set (Var "c"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "a"))) &  "("  (Bool (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "c")))) "implies" (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "c")))  ")"  &  "("  (Bool (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "c")))) "implies" (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "c")))  ")"  &  "("  (Bool (Bool (Set (Var "c"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "b")))) "implies" (Bool (Set (Var "c"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "b")))  ")"  &  "("  (Bool (Bool (Set (Var "c"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "b")))) "implies" (Bool (Set (Var "c"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "b")))  ")"   ")" ))))) ; 
 
theorem :: ARROW:12 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "o")) "," (Set (Var "o9")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_arrow :::"LinOrders"::: )  (Set (Var "A"))) "holds"    "("  (Bool  "not" (Bool  "("   "("  (Bool (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "b")))) "implies" (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "b")))  ")"  &  "("  (Bool (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "b")))) "implies" (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "b")))  ")"  &  "("  (Bool (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "a")))) "implies" (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "a")))  ")"  &  "("  (Bool (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "a")))) "implies" (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "a")))  ")"  & (Bool  "not" (Bool  "("  (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "b"))) "iff" (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "b")))  ")" ))  ")" )) & (Bool  "not" (Bool  "("   "("  (Bool (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "b")))) "implies" (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "b")))  ")"  &  "("  (Bool (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "b")))) "implies" (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "b")))  ")"  & (Bool  "not" (Bool  "("   "("  (Bool (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "b")))) "implies" (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "b")))  ")"  &  "("  (Bool (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "b")))) "implies" (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "b")))  ")"  &  "("  (Bool (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "a")))) "implies" (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "a")))  ")"  &  "("  (Bool (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "a")))) "implies" (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "a")))  ")"   ")" ))  ")" ))  ")" ))) ; 
 
theorem :: ARROW:13 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "o")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_arrow :::"LinOrders"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "o9")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A"))) "holds"   (Bool  "("  (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "b")))) "holds"  (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "b")))  ")" ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o")) "," (Set (Var "b"))) "iff" (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Var "o9")) "," (Set (Var "b")))  ")" ))  ")" )))) ; 
 begin  






































theorem :: ARROW:14 (Bool  "for" (Set (Var "A")) "," (Set (Var "N")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "N")) "," (Set  "("  ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A")) ")" ) ")"  ")" ) "," (Set  "("  ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "p")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "N")) "," (Set  "("  ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A")) ")" ) ")" )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "N"))  "holds" (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "p"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i"))) "," (Set (Var "b")))  ")" )) "holds"  (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p"))) "," (Set (Var "b"))))  ")" ) & (Bool  "("   "for" (Set (Var "p")) "," (Set (Var "p9")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "N")) "," (Set  "("  ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A")) ")" ) ")" )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "N")) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "p"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i"))) "," (Set (Var "b")))) "implies" (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "p9"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i"))) "," (Set (Var "b")))  ")"  &  "("  (Bool (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "p9"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i"))) "," (Set (Var "b")))) "implies" (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "p"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i"))) "," (Set (Var "b")))  ")"  &  "("  (Bool (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "p"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i"))) "," (Set (Var "a")))) "implies" (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "p9"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i"))) "," (Set (Var "a")))  ")"  &  "("  (Bool (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "p9"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i"))) "," (Set (Var "a")))) "implies" (Bool (Set (Var "b"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "p"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i"))) "," (Set (Var "a")))  ")"   ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p"))) "," (Set (Var "b"))) "iff" (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p9"))) "," (Set (Var "b")))  ")" ))  ")" ) & (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">="::: )  (Num 3))) "holds"  (Bool  "ex" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "N")) "st"  (Bool  "for" (Set (Var "p")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "N")) "," (Set  "("  ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A")) ")" ) ")" )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "p"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n"))) "," (Set (Var "b")))) "holds"  (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p"))) "," (Set (Var "b")))))))) ; 
 


















theorem :: ARROW:15 (Bool  "for" (Set (Var "A")) "," (Set (Var "N")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "N")) "," (Set  "("  ($#k3_arrow :::"LinOrders"::: )  (Set (Var "A")) ")" ) ")"  ")" ) "," (Set  "("  ($#k2_arrow :::"LinPreorders"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "p")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "N")) "," (Set  "("  ($#k3_arrow :::"LinOrders"::: )  (Set (Var "A")) ")" ) ")" )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "N"))  "holds" (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "p"))  ($#k1_arrow :::"."::: )  (Set (Var "i"))) "," (Set (Var "b")))  ")" )) "holds"  (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p"))) "," (Set (Var "b"))))  ")" ) & (Bool  "("   "for" (Set (Var "p")) "," (Set (Var "p9")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "N")) "," (Set  "("  ($#k3_arrow :::"LinOrders"::: )  (Set (Var "A")) ")" ) ")" )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "N")) "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "p"))  ($#k1_arrow :::"."::: )  (Set (Var "i"))) "," (Set (Var "b"))) "iff" (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "p9"))  ($#k1_arrow :::"."::: )  (Set (Var "i"))) "," (Set (Var "b")))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p"))) "," (Set (Var "b"))) "iff" (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p9"))) "," (Set (Var "b")))  ")" ))  ")" ) & (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">="::: )  (Num 3))) "holds"  (Bool  "ex" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "N")) "st"  (Bool  "for" (Set (Var "p")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "N")) "," (Set  "("  ($#k3_arrow :::"LinOrders"::: )  (Set (Var "A")) ")" ) ")" )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "p"))  ($#k1_arrow :::"."::: )  (Set (Var "n"))) "," (Set (Var "b"))) "iff" (Bool (Set (Var "a"))  ($#r1_arrow :::"<_"::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p"))) "," (Set (Var "b")))  ")" )))))) ;