:: MEASURE4  semantic presentation begin  








theorem :: MEASURE4:1 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "S")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Var "S"))  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "G"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k8_subset_1 :::"/\"::: )  (Set  "(" (Set (Var "F"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )))  ")" )) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k8_subset_1 :::"/\"::: )  (Set  "("  ($#k3_tarski :::"union"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "F")) ")" ) ")" ))))))) ; 
 
theorem :: MEASURE4:2 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "S")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S"))  "st" (Bool (Bool (Set (Set (Var "G"))  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "G"))  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "F"))  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "G"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )))  ")" )) "holds"  (Bool  "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S"))  "st" (Bool (Bool (Set (Set (Var "H"))  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "H"))  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "F"))  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k6_subset_1 :::"\"::: )  (Set  "(" (Set (Var "G"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )))  ")" )) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "F")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "H")) ")" ))))))) ; 
 
theorem :: MEASURE4:3 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k9_setfam_1 :::"bool"::: )  (Set (Var "X"))) "is"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; mode  :::"C_Measure":::  "of" "X" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k9_setfam_1 :::"bool"::: )  "X" ")" ) "," (Set  ($#k7_numbers :::"ExtREAL"::: ) ) means :: MEASURE4:def 1 (Bool  "("  (Bool it "is" bbbadV6_SUPINF_2()) & (Bool it "is"   ($#v10_valued_0 :::"zeroed"::: )  ) & (Bool  "("   "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "X"  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))) "holds"  (Bool  "("  (Bool (Set it  ($#k12_supinf_2 :::"."::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Set it  ($#k12_supinf_2 :::"."::: )  (Set (Var "B")))) & (Bool  "("   "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "("  ($#k9_setfam_1 :::"bool"::: )  "X" ")" ) "holds"  (Bool (Set it  ($#k12_supinf_2 :::"."::: )  (Set  "("  ($#k5_setfam_1 :::"union"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "F")) ")" ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k19_supinf_2 :::"SUM"::: )  (Set  "(" it  ($#k1_partfun1 :::"*"::: )  (Set (Var "F")) ")" )))  ")" )  ")" )  ")" )  ")" ); end; 





:: deftheorem    defines :::"C_Measure"::: MEASURE4:def 1 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set (Var "X")) ")" ) "," (Set  ($#k7_numbers :::"ExtREAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m1_measure4 :::"C_Measure"::: )   "of" (Set (Var "X"))) "iff" (Bool  "("  (Bool (Set (Var "b2")) "is" bbbadV6_SUPINF_2()) & (Bool (Set (Var "b2")) "is"   ($#v10_valued_0 :::"zeroed"::: )  ) & (Bool  "("   "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "b2"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "b2"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "B")))) & (Bool  "("   "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set (Var "X")) ")" ) "holds"  (Bool (Set (Set (Var "b2"))  ($#k12_supinf_2 :::"."::: )  (Set  "("  ($#k5_setfam_1 :::"union"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "F")) ")" ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k19_supinf_2 :::"SUM"::: )  (Set  "(" (Set (Var "b2"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "F")) ")" )))  ")" )  ")" )  ")" )  ")" )  ")" ))); 
 


definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "C" be    ($#m1_measure4 :::"C_Measure"::: )   "of" (Set (Const "X")); func  :::"sigma_Field"::: "C" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset-Family":::) "of" "X" means :: MEASURE4:def 2 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "X" "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "for" (Set (Var "W")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "X"  "st" (Bool (Bool (Set (Var "W"))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set "X"  ($#k6_subset_1 :::"\"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set  "(" "C"  ($#k12_supinf_2 :::"."::: )  (Set (Var "W")) ")" )  ($#k3_supinf_2 :::"+"::: )  (Set  "(" "C"  ($#k12_supinf_2 :::"."::: )  (Set (Var "Z")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set "C"  ($#k12_supinf_2 :::"."::: )  (Set  "(" (Set (Var "W"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Z")) ")" ))))  ")" )); end; 






:: deftheorem    defines :::"sigma_Field"::: MEASURE4:def 2 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"    ($#m1_measure4 :::"C_Measure"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "b3")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C")))) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool  "for" (Set (Var "W")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "W"))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "C"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "W")) ")" )  ($#k3_supinf_2 :::"+"::: )  (Set  "(" (Set (Var "C"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "Z")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "C"))  ($#k12_supinf_2 :::"."::: )  (Set  "(" (Set (Var "W"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Z")) ")" ))))  ")" ))  ")" )))); 
 
theorem :: MEASURE4:4 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"    ($#m1_measure4 :::"C_Measure"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "W")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "C"))  ($#k12_supinf_2 :::"."::: )  (Set  "(" (Set (Var "W"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Z")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "C"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "W")) ")" )  ($#k3_supinf_2 :::"+"::: )  (Set  "(" (Set (Var "C"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "Z")) ")" )))))) ; 
 
theorem :: MEASURE4:5 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"    ($#m1_measure4 :::"C_Measure"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C")))) "iff" (Bool  "for" (Set (Var "W")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "W"))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "C"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "W")) ")" )  ($#k3_supinf_2 :::"+"::: )  (Set  "(" (Set (Var "C"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "C"))  ($#k12_supinf_2 :::"."::: )  (Set  "(" (Set (Var "W"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Z")) ")" ))))  ")" )))) ; 
 
theorem :: MEASURE4:6 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"    ($#m1_measure4 :::"C_Measure"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "W")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "W"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C")))) & (Bool (Set (Var "Z"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "W")))) "holds"  (Bool (Set (Set (Var "C"))  ($#k12_supinf_2 :::"."::: )  (Set  "(" (Set (Var "W"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "C"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "W")) ")" )  ($#k3_supinf_2 :::"+"::: )  (Set  "(" (Set (Var "C"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "Z")) ")" )))))) ; 
 
theorem :: MEASURE4:7 (Bool  "for" (Set (Var "A")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"    ($#m1_measure4 :::"C_Measure"::: )   "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C"))))) "holds"  (Bool (Set (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "A")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C")))))) ; 
 
theorem :: MEASURE4:8 (Bool  "for" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"    ($#m1_measure4 :::"C_Measure"::: )   "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C")))) & (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C"))))) "holds"  (Bool (Set (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "B")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C")))))) ; 
 
theorem :: MEASURE4:9 (Bool  "for" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"    ($#m1_measure4 :::"C_Measure"::: )   "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C")))) & (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C"))))) "holds"  (Bool (Set (Set (Var "A"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "B")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C")))))) ; 
 
theorem :: MEASURE4:10 (Bool  "for" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"    ($#m1_measure4 :::"C_Measure"::: )   "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C")))) & (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C"))))) "holds"  (Bool (Set (Set (Var "A"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "B")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C")))))) ; 
 
theorem :: MEASURE4:11 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "N")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Var "S")) (Bool  "ex" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "F"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k2_measure1 :::"/\"::: )  (Set  "(" (Set (Var "N"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ))))))))) ; 
 
theorem :: MEASURE4:12 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"    ($#m1_measure4 :::"C_Measure"::: )   "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C"))) "is"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X"))))) ; 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; let "C" be    ($#m1_measure4 :::"C_Measure"::: )   "of" (Set (Const "X")); 
cluster (Set   ($#k1_measure4 :::"sigma_Field"::: )  "C") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_prob_1 :::"compl-closed"::: )     ($#v3_measure1 :::"sigma-additive"::: )   ; 
end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "S" be   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "A" be    ($#m1_measure2 :::"N_Sub_fam"::: )   "of" (Set (Const "S")); :: original: :::"union"::: redefine func  :::"union"::: "A" ->    ($#m2_subset_1 :::"Element"::: )   "of" "S"; end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "C" be    ($#m1_measure4 :::"C_Measure"::: )   "of" (Set (Const "X")); func  :::"sigma_Meas"::: "C" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k1_measure4 :::"sigma_Field"::: )  "C" ")" ) "," (Set  ($#k7_numbers :::"ExtREAL"::: ) ) means :: MEASURE4:def 3 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "X"  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_measure4 :::"sigma_Field"::: )  "C"))) "holds"  (Bool (Set it  ($#k12_supinf_2 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set "C"  ($#k12_supinf_2 :::"."::: )  (Set (Var "A"))))); end; 






:: deftheorem    defines :::"sigma_Meas"::: MEASURE4:def 3 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"    ($#m1_measure4 :::"C_Measure"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C")) ")" ) "," (Set  ($#k7_numbers :::"ExtREAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_measure4 :::"sigma_Meas"::: )  (Set (Var "C")))) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C"))))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "C"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "A")))))  ")" )))); 
 
theorem :: MEASURE4:13 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"    ($#m1_measure4 :::"C_Measure"::: )   "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k3_measure4 :::"sigma_Meas"::: )  (Set (Var "C"))) "is"   ($#m1_subset_1 :::"Measure":::) "of" (Set  "("  ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C")) ")" )))) ; 
 
theorem :: MEASURE4:14 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"    ($#m1_measure4 :::"C_Measure"::: )   "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k3_measure4 :::"sigma_Meas"::: )  (Set (Var "C"))) "is"   ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set  "("  ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C")) ")" )))) ; 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; let "C" be    ($#m1_measure4 :::"C_Measure"::: )   "of" (Set (Const "X")); 
cluster (Set   ($#k3_measure4 :::"sigma_Meas"::: )  "C") ->   ($#v10_valued_0 :::"zeroed"::: )   bbbadV6_SUPINF_2()   ($#v4_measure1 :::"sigma-additive"::: )   ; 
end; 
theorem :: MEASURE4:15 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"    ($#m1_measure4 :::"C_Measure"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Set (Var "C"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_2 :::"0."::: )  ))) "holds"  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C"))))))) ; 
 
theorem :: MEASURE4:16 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"    ($#m1_measure4 :::"C_Measure"::: )   "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k3_measure4 :::"sigma_Meas"::: )  (Set (Var "C")))  ($#r1_measure3 :::"is_complete"::: )  (Set   ($#k1_measure4 :::"sigma_Field"::: )  (Set (Var "C")))))) ;