:: JCT_MISC  semantic presentation begin  scheme  :: JCT_MISC:sch 1 NonEmpty{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool (Bool  "not"  "{"  (Set F2 "(" (Set (Var "a")) ")" ) where a "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) : (Bool verum)  "}"   "is"   ($#v1_xboole_0 :::"empty"::: )  ))
 proof 


end; 







theorem :: JCT_MISC:1 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set (Set  "(" (Set (Var "r"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s")) ")" )  ($#k6_real_1 :::"/"::: )  (Num 2))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) ; 
 
theorem :: JCT_MISC:2 (Bool  "for" (Set (Var "r0")) "," (Set (Var "s0")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "r0"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s0")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "r"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s")) ")" ) ")" ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "r0"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "s0"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s")) ")" ) ")" )))) ; 
 
theorem :: JCT_MISC:3 (Bool  "for" (Set (Var "t")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k2_rcomp_1 :::".["::: ) ))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "t")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "r")) ")" ) "," (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "s")) ")" ) ")" ))) ; 
 scheme  :: JCT_MISC:sch 2 DoubleChoice{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F3() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set F1 "("  ")" ) "," (Set F2 "("  ")" )(Bool  "ex" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set F1 "("  ")" ) "," (Set F3 "("  ")" ) "st"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"  (Bool P1[(Set (Var "i")) "," (Set (Set (Var "a"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i"))) "," (Set (Set (Var "b"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i")))]))))
 provided
(Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) (Bool  "ex" (Set (Var "ai")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" )(Bool  "ex" (Set (Var "bi")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ) "st" (Bool P1[(Set (Var "i")) "," (Set (Var "ai")) "," (Set (Var "bi"))]))))
 proof 


end; 
theorem :: JCT_MISC:4 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "G")))) "holds"  (Bool  "ex" (Set (Var "GS")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))(Bool  "ex" (Set (Var "GT")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "GS")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool (Set (Var "GT")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set (Var "GS")) "," (Set (Var "GT")) ($#k3_borsuk_1 :::":]"::: ) )) & (Bool (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set (Var "GS")) "," (Set (Var "GT")) ($#k3_borsuk_1 :::":]"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "G")))  ")" )))  ")" )) "holds"  (Bool (Set (Var "G")) "is"   ($#v3_pre_topc :::"open"::: )  ))) ; 
 begin  
theorem :: JCT_MISC:5 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#v1_rcomp_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B"))) "is"   ($#v1_rcomp_1 :::"compact"::: )  )) ; 
 
theorem :: JCT_MISC:6 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v1_pscomp_1 :::"continuous"::: )    ($#m1_subset_1 :::"RealMap":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v2_connsp_1 :::"connected"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "A"))) "is"   ($#v6_xxreal_2 :::"interval"::: )  )))) ; 
 definitionlet "A", "B" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); func  :::"dist":::  "(" "A" "," "B" ")"  ->   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   means :: JCT_MISC:def 1 (Bool  "ex" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "r"))  ($#k9_real_1 :::"-"::: )  (Set (Var "s")) ")" ) ")" ) where r, s "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) : (Bool  "("  (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  "A") & (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  "B")  ")" )  "}"  ) & (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X"))))  ")" )); commutativity  
(Bool  "for" (Set (Var "b1")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool  "ex" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "r"))  ($#k9_real_1 :::"-"::: )  (Set (Var "s")) ")" ) ")" ) where r, s "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) : (Bool  "("  (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))  ")" )  "}"  ) & (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X"))))  ")" ))) "holds"  (Bool  "ex" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "r"))  ($#k9_real_1 :::"-"::: )  (Set (Var "s")) ")" ) ")" ) where r, s "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) : (Bool  "("  (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" )  "}"  ) & (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X"))))  ")" ))))
 ; end; 






:: deftheorem    defines :::"dist"::: JCT_MISC:def 1 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "b3")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_jct_misc :::"dist"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) "iff" (Bool  "ex" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "r"))  ($#k9_real_1 :::"-"::: )  (Set (Var "s")) ")" ) ")" ) where r, s "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) : (Bool  "("  (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))  ")" )  "}"  ) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X"))))  ")" ))  ")" ))); 
 
theorem :: JCT_MISC:7 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "r"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s")) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k1_jct_misc :::"dist"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )))) ; 
 
theorem :: JCT_MISC:8 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "C"))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Set (Var "D"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k1_jct_misc :::"dist"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_jct_misc :::"dist"::: )   "(" (Set (Var "C")) "," (Set (Var "D")) ")" )))) ; 
 
theorem :: JCT_MISC:9 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_rcomp_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) (Bool  "ex" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set   ($#k1_jct_misc :::"dist"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "r"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s")) ")" )))  ")" ))) ; 
 
theorem :: JCT_MISC:10 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_rcomp_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k1_jct_misc :::"dist"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: JCT_MISC:11 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_rcomp_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_subset_1 :::"misses"::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k1_jct_misc :::"dist"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: JCT_MISC:12 (Bool  "for" (Set (Var "e")) "," (Set (Var "f")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#v1_rcomp_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B"))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "e")) "," (Set (Var "f")) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "e")) "," (Set (Var "f")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k1_numbers :::"REAL"::: ) ) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set (Var "S"))  ($#k8_nat_1 :::"."::: )  (Set (Var "i"))) "is"   ($#v6_xxreal_2 :::"interval"::: )  ) & (Bool (Set (Set (Var "S"))  ($#k8_nat_1 :::"."::: )  (Set (Var "i")))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "A"))) & (Bool (Set (Set (Var "S"))  ($#k8_nat_1 :::"."::: )  (Set (Var "i")))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "B")))  ")" )  ")" )) "holds"  (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "e")) "," (Set (Var "f")) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Bool  "not" (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B"))))) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) (Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "S"))  ($#k8_nat_1 :::"."::: )  (Set (Var "k"))))  ")" ))  ")" )  ")" ))))) ; 
 
theorem :: JCT_MISC:13 (Bool  "for" (Set (Var "S")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "S")) "is"   ($#v9_rltopsp1 :::"bounded"::: )  )) "holds"  (Bool (Set (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set (Var "S"))) "is"   ($#v2_rcomp_1 :::"closed"::: )  )) ; 
 
theorem :: JCT_MISC:14 (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "S")) "is"   ($#v9_rltopsp1 :::"bounded"::: )  )) "holds"  (Bool (Set (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set (Var "S"))) "is"   ($#v5_xxreal_2 :::"real-bounded"::: )  )) ; 
 
theorem :: JCT_MISC:15 (Bool  "for" (Set (Var "S")) "being"   ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set (Var "S"))) "is"   ($#v1_rcomp_1 :::"compact"::: )  )) ;