:: PROB_1  semantic presentation begin  






























theorem :: PROB_1:1 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool  "ex" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set (Var "seq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Var "r")))))) "holds"  (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set (Var "r")))  ")" ))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "IT" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); attr "IT" is  :::"compl-closed":::  means :: PROB_1:def 1 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "X"  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  "IT")) "holds"  (Bool (Set (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  )  ($#r2_hidden :::"in"::: )  "IT")); end; 





:: deftheorem    defines :::"compl-closed"::: PROB_1:def 1 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_prob_1 :::"compl-closed"::: )  ) "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 (Var "IT")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "IT"))))  ")" ))); 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_zfmisc_1 :::"bool"::: )  "X") ->   ($#v2_finsub_1 :::"cap-closed"::: )   ; 
end; registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_zfmisc_1 :::"bool"::: )  "X") ->   ($#v1_prob_1 :::"compl-closed"::: )    for  ($#m1_subset_1 :::"Subset-Family":::) "of" "X"; 
end; registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_finsub_1 :::"cap-closed"::: )     ($#v1_prob_1 :::"compl-closed"::: )    for    ($#m1_subset_1 :::"Event"::: )   "of" ; 
end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; mode Field_Subset of "X" is  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_finsub_1 :::"cap-closed"::: )     ($#v1_prob_1 :::"compl-closed"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" "X"; end; 



theorem :: PROB_1:2 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_tarski :::"}"::: ) ) "is"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))))) ; 
 
theorem :: PROB_1:3 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "F"))) & (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "B")))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))))) ; 
 
theorem :: PROB_1:4 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "F"))))) ; 
 
theorem :: PROB_1:5 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "F"))))) ; 
 
theorem :: PROB_1:6 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "F"))) & (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k7_subset_1 :::"\"::: )  (Set (Var "B")))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))))) ; 
 
theorem :: PROB_1:7 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "F"))) & (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "B")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "B")))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))))) ; 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," "X" ($#k2_tarski :::"}"::: ) ) ->   ($#v2_finsub_1 :::"cap-closed"::: )   ; 
end; 
theorem :: PROB_1:8 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "X")) ($#k2_tarski :::"}"::: ) ) "is"   ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")))) ; 
 
theorem :: PROB_1:9 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k9_setfam_1 :::"bool"::: )  (Set (Var "X"))) "is"   ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")))) ; 
 
theorem :: PROB_1:10 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "X")) ($#k2_tarski :::"}"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "F"))) & (Bool (Set (Var "F"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_setfam_1 :::"bool"::: )  (Set (Var "X"))))  ")" ))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; mode SetSequence of "X" is   ($#m1_subset_1 :::"sequence":::) "of" (Set  "("  ($#k9_setfam_1 :::"bool"::: )  "X" ")" ); end; 







theorem :: PROB_1:11 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "A1")) ")" )) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "A1" be   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); :: original: :::"Union"::: redefine func  :::"Union"::: "A1" ->   ($#m1_subset_1 :::"Subset":::) "of" "X"; end; 
theorem :: PROB_1:12 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_prob_1 :::"Union"::: )  (Set (Var "A1")))) "iff" (Bool  "ex" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))))  ")" ))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "A1" be   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); func  :::"Complement"::: "A1" ->   ($#m1_subset_1 :::"SetSequence":::) "of" "X" means :: PROB_1:def 2 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set it  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "A1"  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k3_subset_1 :::"`"::: )  ))); involutiveness  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "b2")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X"))  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "b1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "b2"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k3_subset_1 :::"`"::: )  ))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "b2"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "b1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k3_subset_1 :::"`"::: )  ))))
 ; end; 






:: deftheorem    defines :::"Complement"::: PROB_1:def 2 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A1")) "," (Set (Var "b3")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_prob_1 :::"Complement"::: )  (Set (Var "A1")))) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "b3"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k3_subset_1 :::"`"::: )  )))  ")" ))); 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "A1" be   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); func  :::"Intersection"::: "A1" ->   ($#m1_subset_1 :::"Subset":::) "of" "X" equals :: PROB_1:def 3 (Set (Set  "("  ($#k1_prob_1 :::"Union"::: )  (Set  "("  ($#k2_prob_1 :::"Complement"::: )  "A1" ")" ) ")" )  ($#k3_subset_1 :::"`"::: )  ); end; 






:: deftheorem    defines :::"Intersection"::: PROB_1:def 3 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k3_prob_1 :::"Intersection"::: )  (Set (Var "A1")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_prob_1 :::"Union"::: )  (Set  "("  ($#k2_prob_1 :::"Complement"::: )  (Set (Var "A1")) ")" ) ")" )  ($#k3_subset_1 :::"`"::: )  )))); 
 
theorem :: PROB_1:13 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_prob_1 :::"Intersection"::: )  (Set (Var "A1")))) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))))  ")" ))) ; 
 
theorem :: PROB_1:14 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k3_prob_1 :::"Intersection"::: )  (Set  "(" (Set (Var "A"))  ($#k12_funct_7 :::"followed_by"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")))))) ; 
 definitionlet "f" be   ($#m1_hidden :::"Function":::); attr "f" is  :::"non-ascending":::  means :: PROB_1:def 4 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set "f"  ($#k1_funct_1 :::"."::: )  (Set (Var "m")))  ($#r1_tarski :::"c="::: )  (Set "f"  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))))); attr "f" is  :::"non-descending":::  means :: PROB_1:def 5 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set "f"  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_tarski :::"c="::: )  (Set "f"  ($#k1_funct_1 :::"."::: )  (Set (Var "m"))))); end; 








:: deftheorem    defines :::"non-ascending"::: PROB_1:def 4 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_prob_1 :::"non-ascending"::: )  ) "iff" (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "m")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))))  ")" )); 
 
:: deftheorem    defines :::"non-descending"::: PROB_1:def 5 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_prob_1 :::"non-descending"::: )  ) "iff" (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "m")))))  ")" )); 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "F" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); attr "F" is  :::"sigma-multiplicative":::  means :: PROB_1:def 6 (Bool  "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" "X"  "st" (Bool (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "A1")))  ($#r1_tarski :::"c="::: )  "F")) "holds"  (Bool (Set   ($#k3_prob_1 :::"Intersection"::: )  (Set (Var "A1")))  ($#r2_hidden :::"in"::: )  "F")); end; 





:: deftheorem    defines :::"sigma-multiplicative"::: PROB_1:def 6 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v4_prob_1 :::"sigma-multiplicative"::: )  ) "iff" (Bool  "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "A1")))  ($#r1_tarski :::"c="::: )  (Set (Var "F")))) "holds"  (Bool (Set   ($#k3_prob_1 :::"Intersection"::: )  (Set (Var "A1")))  ($#r2_hidden :::"in"::: )  (Set (Var "F"))))  ")" ))); 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_zfmisc_1 :::"bool"::: )  "X") ->   ($#v4_prob_1 :::"sigma-multiplicative"::: )    for  ($#m1_subset_1 :::"Subset-Family":::) "of" "X"; 
end; registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_prob_1 :::"compl-closed"::: )     ($#v4_prob_1 :::"sigma-multiplicative"::: )    for    ($#m1_subset_1 :::"Event"::: )   "of" ; 
end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; mode SigmaField of "X" is  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_prob_1 :::"compl-closed"::: )     ($#v4_prob_1 :::"sigma-multiplicative"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" "X"; end; 
theorem :: PROB_1:15 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "S")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X"))) "iff" (Bool  "("  (Bool (Set (Var "S"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_setfam_1 :::"bool"::: )  (Set (Var "X")))) & (Bool  "("   "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "A1")))  ($#r1_tarski :::"c="::: )  (Set (Var "S")))) "holds"  (Bool (Set   ($#k3_prob_1 :::"Intersection"::: )  (Set (Var "A1")))  ($#r2_hidden :::"in"::: )  (Set (Var "S")))  ")" ) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "S")))  ")" )  ")" )  ")" ))) ; 
 
theorem :: PROB_1:16 (Bool  "for" (Set (Var "Y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y")) "is"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")))) "holds"  (Bool (Set (Var "Y")) "is"   ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")))) ; 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_prob_1 :::"compl-closed"::: )     ($#v4_prob_1 :::"sigma-multiplicative"::: )    ->   ($#v2_finsub_1 :::"cap-closed"::: )    for    ($#m1_subset_1 :::"Event"::: )   "of" ; 
end; 





registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; let "F" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   "F"  ($#v5_relat_1 :::"-valued"::: )   (Set   ($#k9_setfam_1 :::"bool"::: )  "X")  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set   ($#k5_numbers :::"NAT"::: )  ) "," (Set   ($#k9_setfam_1 :::"bool"::: )  "X"))  for    ($#m1_subset_1 :::"Event"::: )   "of" ; 
end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "F" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); mode SetSequence of "F" is "F"  ($#v5_relat_1 :::"-valued"::: )    ($#m1_subset_1 :::"SetSequence":::) "of" "X"; end; 
theorem :: PROB_1:17 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Si")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "ASeq")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds"  (Bool (Set   ($#k1_prob_1 :::"Union"::: )  (Set (Var "ASeq")))  ($#r2_hidden :::"in"::: )  (Set (Var "Si")))))) ; 
 notationlet "X" be    ($#m1_hidden :::"set"::: )  ; let "F" be   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); synonym  :::"Event":::  "of" "F" for  :::"Element":::  "of" "X"; end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "F" be   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); :: original: :::"Event"::: redefine mode  :::"Event":::  "of" "F" ->   ($#m1_subset_1 :::"Subset":::) "of" "X"; end; 
theorem :: PROB_1:18 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Si")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Si")))) "holds"  (Bool (Set (Var "x")) "is"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Si"))))) ; 
 
theorem :: PROB_1:19 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Si")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Si")) "holds"  (Bool (Set (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B"))) "is"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Si")))))) ; 
 
theorem :: PROB_1:20 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Si")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "A")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Si")) "holds"  (Bool (Set (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ) "is"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Si")))))) ; 
 
theorem :: PROB_1:21 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Si")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Si")) "holds"  (Bool (Set (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B"))) "is"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Si")))))) ; 
 
theorem :: PROB_1:22 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Si")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  ) "is"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Si"))))) ; 
 
theorem :: PROB_1:23 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Si")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "X")) "is"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Si"))))) ; 
 
theorem :: PROB_1:24 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Si")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Si")) "holds"  (Bool (Set (Set (Var "A"))  ($#k7_subset_1 :::"\"::: )  (Set (Var "B"))) "is"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Si")))))) ; 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; let "Si" be   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); 
cluster   ($#v1_xboole_0 :::"empty"::: )    for    ($#m1_subset_1 :::"Event"::: )   "of" ; 
end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "Si" be   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); func  :::"[#]"::: "Si" ->    ($#m1_prob_1 :::"Event"::: )   "of" "Si" equals :: PROB_1:def 7 "X"; end; 






:: deftheorem    defines :::"[#]"::: PROB_1:def 7 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Si")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k4_prob_1 :::"[#]"::: )  (Set (Var "Si")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))))); 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "Si" be   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "A", "B" be    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Const "Si")); :: original: :::"/\"::: redefine func "A" :::"/\"::: "B" ->    ($#m1_prob_1 :::"Event"::: )   "of" "Si"; :: original: :::"\/"::: redefine func "A" :::"\/"::: "B" ->    ($#m1_prob_1 :::"Event"::: )   "of" "Si"; :: original: :::"\"::: redefine func "A" :::"\"::: "B" ->    ($#m1_prob_1 :::"Event"::: )   "of" "Si"; end; 
theorem :: PROB_1:25 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "Si")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "A1")) "is"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si"))) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "A1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n"))) "is"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Si"))))  ")" )))) ; 
 
theorem :: PROB_1:26 (Bool  "for" (Set (Var "Omega")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "ASeq")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Omega"))  (Bool  "for" (Set (Var "Sigma")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega"))  "st" (Bool (Bool (Set (Var "ASeq")) "is"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")))) "holds"  (Bool (Set   ($#k1_prob_1 :::"Union"::: )  (Set (Var "ASeq"))) "is"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma")))))) ; 
 







theorem :: PROB_1:27 (Bool  "for" (Set (Var "Omega")) "," (Set (Var "p")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Sigma")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "Sigma"))) & (Bool  "("   "for" (Set (Var "D")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega"))  "st" (Bool (Bool (Set (Var "D"))  ($#r2_hidden :::"in"::: )  (Set (Var "Sigma")))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "D")))) "implies" (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "D")))  ($#r1_hidden :::"="::: )  (Num 1))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "D"))))) "implies" (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "D")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"   ")" )  ")" )  ")" )))) ; 
 



theorem :: PROB_1:28 (Bool  "for" (Set (Var "Omega")) "," (Set (Var "p")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Sigma")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Sigma")) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "st"  (Bool  "for" (Set (Var "D")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega"))  "st" (Bool (Bool (Set (Var "D"))  ($#r2_hidden :::"in"::: )  (Set (Var "Sigma")))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "D")))) "implies" (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "D")))  ($#r1_hidden :::"="::: )  (Num 1))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "D"))))) "implies" (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "D")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"   ")" ))))) ; 
 
theorem :: PROB_1:29 (Bool  "for" (Set (Var "Omega")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Sigma")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega"))  (Bool  "for" (Set (Var "ASeq")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Sigma")) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set (Set (Var "P"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "ASeq"))) "is"   ($#m1_subset_1 :::"Real_Sequence":::)))))) ; 
 definitionlet "Omega" be    ($#m1_hidden :::"set"::: )  ; let "Sigma" be   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "ASeq" be   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "Sigma")); let "P" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Sigma")) "," (Set  ($#k1_numbers :::"REAL"::: ) ); :: original: :::"*"::: redefine func "P" :::"*"::: "ASeq" ->   ($#m1_subset_1 :::"Real_Sequence":::); end; 






















definitionlet "Omega" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "Sigma" be   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); mode  :::"Probability":::  "of" "Sigma" ->   ($#m1_subset_1 :::"Function":::) "of" "Sigma" "," (Set  ($#k1_numbers :::"REAL"::: ) ) means :: PROB_1:def 8 (Bool  "("  (Bool  "("   "for" (Set (Var "A")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" "Sigma" "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set it  ($#k1_seq_1 :::"."::: )  (Set (Var "A"))))  ")" ) & (Bool (Set it  ($#k1_seq_1 :::"."::: )  "Omega")  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" "Sigma"  "st" (Bool (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B")))) "holds"  (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k6_prob_1 :::"\/"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" it  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" it  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "ASeq")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" "Sigma"  "st" (Bool (Bool (Set (Var "ASeq")) "is"   ($#v2_prob_1 :::"non-ascending"::: )  )) "holds"  (Bool  "("  (Bool (Set it  ($#k8_prob_1 :::"*"::: )  (Set (Var "ASeq"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "(" it  ($#k8_prob_1 :::"*"::: )  (Set (Var "ASeq")) ")" ))  ($#r1_hidden :::"="::: )  (Set it  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k3_prob_1 :::"Intersection"::: )  (Set (Var "ASeq")) ")" )))  ")" )  ")" )  ")" ); end; 






:: deftheorem    defines :::"Probability"::: PROB_1:def 8 :  (Bool  "for" (Set (Var "Omega")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Sigma")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Sigma")) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b3")) "is"    ($#m2_prob_1 :::"Probability"::: )   "of" (Set (Var "Sigma"))) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "A")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma")) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "b3"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A"))))  ")" ) & (Bool (Set (Set (Var "b3"))  ($#k1_seq_1 :::"."::: )  (Set (Var "Omega")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k6_prob_1 :::"\/"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "b3"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "b3"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "ASeq")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma"))  "st" (Bool (Bool (Set (Var "ASeq")) "is"   ($#v2_prob_1 :::"non-ascending"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set (Var "b3"))  ($#k8_prob_1 :::"*"::: )  (Set (Var "ASeq"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "(" (Set (Var "b3"))  ($#k8_prob_1 :::"*"::: )  (Set (Var "ASeq")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b3"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k3_prob_1 :::"Intersection"::: )  (Set (Var "ASeq")) ")" )))  ")" )  ")" )  ")" )  ")" )))); 
 


registrationlet "Omega" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "Sigma" be   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); 
cluster   ->   ($#v10_valued_0 :::"zeroed"::: )    for    ($#m2_prob_1 :::"Probability"::: )   "of" "Sigma"; 
end; 
theorem :: PROB_1:30 (Bool  "for" (Set (Var "Omega")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Sigma")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega"))  (Bool  "for" (Set (Var "P")) "being"    ($#m2_prob_1 :::"Probability"::: )   "of" (Set (Var "Sigma")) "holds"  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k4_prob_1 :::"[#]"::: )  (Set (Var "Sigma")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))))) ; 
 
theorem :: PROB_1:31 (Bool  "for" (Set (Var "Omega")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Sigma")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega"))  (Bool  "for" (Set (Var "A")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  (Bool  "for" (Set (Var "P")) "being"    ($#m2_prob_1 :::"Probability"::: )   "of" (Set (Var "Sigma")) "holds"  (Bool (Set (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "("  ($#k4_prob_1 :::"[#]"::: )  (Set (Var "Sigma")) ")" )  ($#k7_prob_1 :::"\"::: )  (Set (Var "A")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)))))) ; 
 
theorem :: PROB_1:32 (Bool  "for" (Set (Var "Omega")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Sigma")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega"))  (Bool  "for" (Set (Var "A")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  (Bool  "for" (Set (Var "P")) "being"    ($#m2_prob_1 :::"Probability"::: )   "of" (Set (Var "Sigma")) "holds"  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "("  ($#k4_prob_1 :::"[#]"::: )  (Set (Var "Sigma")) ")" )  ($#k7_prob_1 :::"\"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" ))))))) ; 
 
theorem :: PROB_1:33 (Bool  "for" (Set (Var "Omega")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Sigma")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  (Bool  "for" (Set (Var "P")) "being"    ($#m2_prob_1 :::"Probability"::: )   "of" (Set (Var "Sigma"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "B"))  ($#k7_prob_1 :::"\"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" ))))))) ; 
 
theorem :: PROB_1:34 (Bool  "for" (Set (Var "Omega")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Sigma")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  (Bool  "for" (Set (Var "P")) "being"    ($#m2_prob_1 :::"Probability"::: )   "of" (Set (Var "Sigma"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")))))))) ; 
 
theorem :: PROB_1:35 (Bool  "for" (Set (Var "Omega")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Sigma")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega"))  (Bool  "for" (Set (Var "A")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  (Bool  "for" (Set (Var "P")) "being"    ($#m2_prob_1 :::"Probability"::: )   "of" (Set (Var "Sigma")) "holds"  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)))))) ; 
 
theorem :: PROB_1:36 (Bool  "for" (Set (Var "Omega")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Sigma")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  (Bool  "for" (Set (Var "P")) "being"    ($#m2_prob_1 :::"Probability"::: )   "of" (Set (Var "Sigma")) "holds"  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k6_prob_1 :::"\/"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "B"))  ($#k7_prob_1 :::"\"::: )  (Set (Var "A")) ")" ) ")" ))))))) ; 
 
theorem :: PROB_1:37 (Bool  "for" (Set (Var "Omega")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Sigma")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  (Bool  "for" (Set (Var "P")) "being"    ($#m2_prob_1 :::"Probability"::: )   "of" (Set (Var "Sigma")) "holds"  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k6_prob_1 :::"\/"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "B"))  ($#k7_prob_1 :::"\"::: )  (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B")) ")" ) ")" ) ")" ))))))) ; 
 
theorem :: PROB_1:38 (Bool  "for" (Set (Var "Omega")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Sigma")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  (Bool  "for" (Set (Var "P")) "being"    ($#m2_prob_1 :::"Probability"::: )   "of" (Set (Var "Sigma")) "holds"  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k6_prob_1 :::"\/"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B")) ")" ) ")" ))))))) ; 
 
theorem :: PROB_1:39 (Bool  "for" (Set (Var "Omega")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Sigma")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  (Bool  "for" (Set (Var "P")) "being"    ($#m2_prob_1 :::"Probability"::: )   "of" (Set (Var "Sigma")) "holds"  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k6_prob_1 :::"\/"::: )  (Set (Var "B")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" ))))))) ; 
 






theorem :: PROB_1:40 (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 "Omega" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "X" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "Omega")); func  :::"sigma"::: "X" ->   ($#m1_subset_1 :::"SigmaField":::) "of" "Omega" means :: PROB_1:def 9 (Bool  "("  (Bool "X"  ($#r1_tarski :::"c="::: )  it) & (Bool  "("   "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool "X"  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set (Var "Z")) "is"   ($#m1_subset_1 :::"SigmaField":::) "of" "Omega")) "holds"  (Bool it  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))  ")" )  ")" ); end; 






:: deftheorem    defines :::"sigma"::: PROB_1:def 9 :  (Bool  "for" (Set (Var "Omega")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_prob_1 :::"sigma"::: )  (Set (Var "X")))) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "b3"))) & (Bool  "("   "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set (Var "Z")) "is"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")))) "holds"  (Bool (Set (Var "b3"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))  ")" )  ")" )  ")" )))); 
 definitionlet "r" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"halfline"::: "r" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) equals :: PROB_1:def 10 (Set  ($#k4_xxreal_1 :::"]."::: ) (Set  ($#k2_xxreal_0 :::"-infty"::: ) ) "," "r" ($#k4_xxreal_1 :::".["::: ) ); end; 





:: deftheorem    defines :::"halfline"::: PROB_1:def 10 :  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k10_prob_1 :::"halfline"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_xxreal_1 :::"]."::: ) (Set  ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "r")) ($#k4_xxreal_1 :::".["::: ) ))); 
 definitionfunc  :::"Family_of_halflines":::  ->   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) equals :: PROB_1:def 11  "{"  (Set  "("  ($#k10_prob_1 :::"halfline"::: )  (Set (Var "r")) ")" ) where r "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) : (Bool verum)  "}"  ; end; 




:: deftheorem    defines :::"Family_of_halflines"::: PROB_1:def 11 :  (Bool (Set   ($#k11_prob_1 :::"Family_of_halflines"::: )  )  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k10_prob_1 :::"halfline"::: )  (Set (Var "r")) ")" ) where r "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) : (Bool verum)  "}"  ); 
 definitionfunc  :::"Borel_Sets":::  ->   ($#m1_subset_1 :::"SigmaField":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) equals :: PROB_1:def 12 (Set   ($#k9_prob_1 :::"sigma"::: )  (Set  ($#k11_prob_1 :::"Family_of_halflines"::: ) )); end; 




:: deftheorem    defines :::"Borel_Sets"::: PROB_1:def 12 :  (Bool (Set   ($#k12_prob_1 :::"Borel_Sets"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k9_prob_1 :::"sigma"::: )  (Set  ($#k11_prob_1 :::"Family_of_halflines"::: ) ))); 
 
theorem :: PROB_1:41 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k2_prob_1 :::"Complement"::: )  (Set  "(" (Set (Var "A"))  ($#k12_funct_7 :::"followed_by"::: )  (Set (Var "B")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ")" )  ($#k12_funct_7 :::"followed_by"::: )  (Set  "(" (Set (Var "B"))  ($#k3_subset_1 :::"`"::: )  ")" ))))) ; 
 definitionlet "X", "Y" be    ($#m1_hidden :::"set"::: )  ; let "A" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); let "F" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Y")) "," (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set (Const "A")) ")" ); let "x" be    ($#m1_hidden :::"set"::: )  ; :: original: :::"."::: redefine func "F" :::"."::: "x" ->   ($#m1_subset_1 :::"Subset-Family":::) "of" "X"; end;