:: MEASURE5  semantic presentation begin  



scheme  :: MEASURE5:sch 1 RSetEq{ P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "X1")) "," (Set (Var "X2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X1"))) "iff" (Bool P1[(Set (Var "x"))])  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X2"))) "iff" (Bool P1[(Set (Var "x"))])  ")" )  ")" )) "holds"  (Bool (Set (Var "X1"))  ($#r1_hidden :::"="::: )  (Set (Var "X2"))))
 proof 


end; definitionlet "a", "b" be   ($#m1_subset_1 :::"R_eal":::); :: original: :::"]."::: redefine func :::"].":::"a" "," "b":::".["::: ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) means :: MEASURE5:def 1 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool "a"  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  "b")  ")" )  ")" )); end; 






:: deftheorem    defines :::"]."::: MEASURE5:def 1 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"R_eal":::)  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_measure5 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_measure5 :::".["::: ) )) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))  ")" )  ")" ))  ")" ))); 
 definitionlet "IT" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); attr "IT" is  :::"open_interval":::  means :: MEASURE5:def 2 (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"R_eal":::) "st" (Bool "IT"  ($#r1_hidden :::"="::: )  (Set  ($#k1_measure5 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_measure5 :::".["::: ) ))); attr "IT" is  :::"closed_interval":::  means :: MEASURE5:def 3 (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st" (Bool "IT"  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))); end; 








:: deftheorem    defines :::"open_interval"::: MEASURE5:def 2 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_measure5 :::"open_interval"::: )  ) "iff" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Set (Var "IT"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_measure5 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_measure5 :::".["::: ) )))  ")" )); 
 
:: deftheorem    defines :::"closed_interval"::: MEASURE5:def 3 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_measure5 :::"closed_interval"::: )  ) "iff" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st" (Bool (Set (Var "IT"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )))  ")" )); 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_membered :::"complex-membered"::: )     ($#v2_membered :::"ext-real-membered"::: )     ($#v3_membered :::"real-membered"::: )     ($#v1_measure5 :::"open_interval"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  ($#k1_numbers :::"REAL"::: ) ))); 

cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_membered :::"complex-membered"::: )     ($#v2_membered :::"ext-real-membered"::: )     ($#v3_membered :::"real-membered"::: )     ($#v2_measure5 :::"closed_interval"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  ($#k1_numbers :::"REAL"::: ) ))); 
end; definitionlet "IT" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); attr "IT" is  :::"right_open_interval":::  means :: MEASURE5:def 4 (Bool  "ex" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  (Bool  "ex" (Set (Var "b")) "being"   ($#m1_subset_1 :::"R_eal":::) "st" (Bool "IT"  ($#r1_hidden :::"="::: )  (Set  ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_rcomp_1 :::".["::: ) )))); end; 




:: deftheorem    defines :::"right_open_interval"::: MEASURE5:def 4 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v3_measure5 :::"right_open_interval"::: )  ) "iff" (Bool  "ex" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  (Bool  "ex" (Set (Var "b")) "being"   ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Set (Var "IT"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_rcomp_1 :::".["::: ) ))))  ")" )); 
 notationlet "IT" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); synonym  :::"left_closed_interval"::: "IT" for  :::"right_open_interval"::: ; end; definitionlet "IT" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); attr "IT" is  :::"left_open_interval":::  means :: MEASURE5:def 5 (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"R_eal":::)(Bool  "ex" (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st" (Bool "IT"  ($#r1_hidden :::"="::: )  (Set  ($#k4_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_rcomp_1 :::".]"::: ) )))); end; 




:: deftheorem    defines :::"left_open_interval"::: MEASURE5:def 5 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v4_measure5 :::"left_open_interval"::: )  ) "iff" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"R_eal":::)(Bool  "ex" (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st" (Bool (Set (Var "IT"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_rcomp_1 :::".]"::: ) ))))  ")" )); 
 notationlet "IT" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); synonym  :::"right_closed_interval"::: "IT" for  :::"left_open_interval"::: ; end; registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_membered :::"complex-membered"::: )     ($#v2_membered :::"ext-real-membered"::: )     ($#v3_membered :::"real-membered"::: )     ($#v3_measure5 :::"right_open_interval"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  ($#k1_numbers :::"REAL"::: ) ))); 

cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_membered :::"complex-membered"::: )     ($#v2_membered :::"ext-real-membered"::: )     ($#v3_membered :::"real-membered"::: )     ($#v4_measure5 :::"left_open_interval"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  ($#k1_numbers :::"REAL"::: ) ))); 
end; definitionmode Interval is   ($#v6_xxreal_2 :::"interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); end; 



registration
cluster   ($#v1_measure5 :::"open_interval"::: )    ->   ($#v6_xxreal_2 :::"interval"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  ($#k1_numbers :::"REAL"::: ) ))); 

cluster   ($#v2_measure5 :::"closed_interval"::: )    ->   ($#v6_xxreal_2 :::"interval"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  ($#k1_numbers :::"REAL"::: ) ))); 

cluster   ($#v3_measure5 :::"right_open_interval"::: )    ->   ($#v6_xxreal_2 :::"interval"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  ($#k1_numbers :::"REAL"::: ) ))); 

cluster   ($#v4_measure5 :::"left_open_interval"::: )    ->   ($#v6_xxreal_2 :::"interval"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  ($#k1_numbers :::"REAL"::: ) ))); 
end; 
theorem :: MEASURE5:1 (Bool  "for" (Set (Var "I")) "being"   ($#v6_xxreal_2 :::"interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "holds"  (Bool  "("  (Bool (Set (Var "I")) "is"   ($#v1_measure5 :::"open_interval"::: )  ) "or" (Bool (Set (Var "I")) "is"   ($#v2_measure5 :::"closed_interval"::: )  ) "or" (Bool (Set (Var "I")) "is"   ($#v3_measure5 :::"right_open_interval"::: )  ) "or" (Bool (Set (Var "I")) "is"   ($#v4_measure5 :::"left_open_interval"::: )  )  ")" )) ; 
 
theorem :: MEASURE5:2 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))  ")" ))) ; 
 
theorem :: MEASURE5:3 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "c")))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "c"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))  ")" ))) ; 
 
theorem :: MEASURE5:4 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "c")))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "c"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))  ")" ))) ; 
 definitionlet "A" be   ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )  ; func  :::"diameter"::: "A" ->   ($#m1_subset_1 :::"R_eal":::) equals :: MEASURE5:def 6 (Set (Set  "("  ($#k8_supinf_2 :::"sup"::: )  "A" ")" )  ($#k4_supinf_2 :::"-"::: )  (Set  "("  ($#k7_supinf_2 :::"inf"::: )  "A" ")" )) if (Bool "A"  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  otherwise (Set   ($#k1_supinf_2 :::"0."::: )  ); end; 





:: deftheorem    defines :::"diameter"::: MEASURE5:def 6 :  (Bool  "for" (Set (Var "A")) "being"   ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (Bool (Set   ($#k2_measure5 :::"diameter"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k8_supinf_2 :::"sup"::: )  (Set (Var "A")) ")" )  ($#k4_supinf_2 :::"-"::: )  (Set  "("  ($#k7_supinf_2 :::"inf"::: )  (Set (Var "A")) ")" )))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) "implies" (Bool (Set   ($#k2_measure5 :::"diameter"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_2 :::"0."::: )  ))  ")"   ")" )); 
 
theorem :: MEASURE5:5 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))) "implies" (Bool (Set   ($#k2_measure5 :::"diameter"::: )  (Set  ($#k1_measure5 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_measure5 :::".["::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k4_supinf_2 :::"-"::: )  (Set (Var "a"))))  ")"  &  "("  (Bool (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) "implies" (Bool (Set   ($#k2_measure5 :::"diameter"::: )  (Set  ($#k1_measure5 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_measure5 :::".["::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_2 :::"0."::: )  ))  ")"   ")" )) ; 
 
theorem :: MEASURE5:6 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "implies" (Bool (Set   ($#k2_measure5 :::"diameter"::: )  (Set  ($#k1_xxreal_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_xxreal_1 :::".]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k4_supinf_2 :::"-"::: )  (Set (Var "a"))))  ")"  &  "("  (Bool (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a")))) "implies" (Bool (Set   ($#k2_measure5 :::"diameter"::: )  (Set  ($#k1_xxreal_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_xxreal_1 :::".]"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_2 :::"0."::: )  ))  ")"   ")" )) ; 
 
theorem :: MEASURE5:7 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))) "implies" (Bool (Set   ($#k2_measure5 :::"diameter"::: )  (Set  ($#k2_xxreal_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_xxreal_1 :::".["::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k4_supinf_2 :::"-"::: )  (Set (Var "a"))))  ")"  &  "("  (Bool (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) "implies" (Bool (Set   ($#k2_measure5 :::"diameter"::: )  (Set  ($#k2_xxreal_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_xxreal_1 :::".["::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_2 :::"0."::: )  ))  ")"   ")" )) ; 
 
theorem :: MEASURE5:8 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))) "implies" (Bool (Set   ($#k2_measure5 :::"diameter"::: )  (Set  ($#k3_xxreal_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_xxreal_1 :::".]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k4_supinf_2 :::"-"::: )  (Set (Var "a"))))  ")"  &  "("  (Bool (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) "implies" (Bool (Set   ($#k2_measure5 :::"diameter"::: )  (Set  ($#k3_xxreal_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_xxreal_1 :::".]"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_2 :::"0."::: )  ))  ")"   ")" )) ; 
 
theorem :: MEASURE5:9 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Interval":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_supinf_1 :::"-infty"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  )) & (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_measure5 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_measure5 :::".["::: ) )) "or" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_xxreal_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_xxreal_1 :::".]"::: ) )) "or" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_xxreal_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_xxreal_1 :::".["::: ) )) "or" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_xxreal_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_xxreal_1 :::".]"::: ) ))  ")" )) "holds"  (Bool (Set   ($#k2_measure5 :::"diameter"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  )))) ; 
 registration
cluster   ($#v1_xboole_0 :::"empty"::: )    ->   ($#v1_measure5 :::"open_interval"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  ($#k1_numbers :::"REAL"::: ) ))); 
end; 
theorem :: MEASURE5:10 (Bool (Set   ($#k2_measure5 :::"diameter"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_2 :::"0."::: )  )) ; 
 
theorem :: MEASURE5:11 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"R_eal":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Interval":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B"))) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_xxreal_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_xxreal_1 :::".]"::: ) )) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) "holds"  (Bool  "("  (Bool (Set   ($#k2_measure5 :::"diameter"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_2 :::"0."::: )  )) & (Bool (Set   ($#k2_measure5 :::"diameter"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_2 :::"0."::: )  ))  ")" ))) ; 
 
theorem :: MEASURE5:12 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Interval":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k2_measure5 :::"diameter"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k2_measure5 :::"diameter"::: )  (Set (Var "B"))))) ; 
 
theorem :: MEASURE5:13 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Interval":::) "holds"  (Bool (Set   ($#k1_supinf_2 :::"0."::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k2_measure5 :::"diameter"::: )  (Set (Var "A"))))) ; 
 
theorem :: MEASURE5:14 (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool  "("  (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set (Var "X")) "is"   ($#v2_measure5 :::"closed_interval"::: )  )  ")" ) "iff" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))  ")" ))  ")" )) ;