:: JGRAPH_8  semantic presentation begin  


















registrationlet "a", "b", "c", "d" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: )   "(" "a" "," "b" "," "c" "," "d" ")" ) ->   ($#v1_convex1 :::"convex"::: )   ; 
end; registrationlet "a", "b", "c", "d" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k1_topreala :::"Trectangle"::: )   "(" "a" "," "b" "," "c" "," "d" ")" ) ->   ($#v1_topalg_2 :::"convex"::: )   ; 
end; 
theorem :: JGRAPH_8:1 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "e")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "g")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k17_borsuk_1 :::"I[01]"::: ) ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) (Bool  "ex" (Set (Var "h")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "h")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Num 5)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "h")))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "h")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k17_borsuk_1 :::"I[01]"::: ) ))) & (Bool (Set (Var "h")) "is"   ($#v5_valued_0 :::"increasing"::: )  ) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Q")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k17_borsuk_1 :::"I[01]"::: ) )  (Bool  "for" (Set (Var "W")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "h")))) & (Bool (Set (Var "Q"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "(" (Set (Var "h"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) "," (Set  "(" (Set (Var "h"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "W"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "Q"))))) "holds"  (Bool (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "W")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "e")))))  ")" )  ")" ))))) ; 
 
theorem :: JGRAPH_8:2 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Var "p1"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "p2"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "P")) "is"   ($#v2_connsp_1 :::"connected"::: )  )) "holds"  (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ))))) ; 
 
theorem :: JGRAPH_8:3 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "g")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "p1")) "," (Set (Var "p2"))  "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ))) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ))))) ; 
 
theorem :: JGRAPH_8:4 (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "f")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "p1")) "," (Set (Var "p2"))  (Bool  "for" (Set (Var "g")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "q1")) "," (Set (Var "q2"))  "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "P"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Var "Q"))) & (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "P")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  ))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "Q")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  ))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "P")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "q1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "q2"))  ($#k18_euclid :::"`2"::: )  ))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "Q")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "q1"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "q2"))  ($#k18_euclid :::"`2"::: )  ))  ")" )  ")" )) "holds"  (Bool (Set (Var "P"))  ($#r2_subset_1 :::"meets"::: )  (Set (Var "Q"))))))) ; 
 
theorem :: JGRAPH_8:5 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k17_borsuk_1 :::"I[01]"::: ) ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "O")) "," (Set (Var "I")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k17_borsuk_1 :::"I[01]"::: ) )  "st" (Bool (Bool (Set (Var "O"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "I"))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "O")) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "I")) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "O")) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "c"))) & (Bool (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "I")) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "d"))) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k17_borsuk_1 :::"I[01]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "d"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "r")) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "d")))  ")" )  ")" )) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r2_subset_1 :::"meets"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g"))))))) ; 
 
theorem :: JGRAPH_8:6 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "ar")) "," (Set (Var "br")) "," (Set (Var "cr")) "," (Set (Var "dr")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k1_topreala :::"Trectangle"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")"  ")" )  (Bool  "for" (Set (Var "h")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "ar")) "," (Set (Var "br"))  (Bool  "for" (Set (Var "v")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "dr")) "," (Set (Var "cr"))  (Bool  "for" (Set (Var "Ar")) "," (Set (Var "Br")) "," (Set (Var "Cr")) "," (Set (Var "Dr")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Set (Var "Ar"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "Br"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Set (Var "Cr"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "c"))) & (Bool (Set (Set (Var "Dr"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "d"))) & (Bool (Set (Var "ar"))  ($#r1_hidden :::"="::: )  (Set (Var "Ar"))) & (Bool (Set (Var "br"))  ($#r1_hidden :::"="::: )  (Set (Var "Br"))) & (Bool (Set (Var "cr"))  ($#r1_hidden :::"="::: )  (Set (Var "Cr"))) & (Bool (Set (Var "dr"))  ($#r1_hidden :::"="::: )  (Set (Var "Dr")))) "holds"  (Bool  "ex" (Set (Var "s")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k17_borsuk_1 :::"I[01]"::: ) ) "st" (Bool (Set (Set (Var "h"))  ($#k3_funct_2 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "v"))  ($#k3_funct_2 :::"."::: )  (Set (Var "t")))))))))) ;