:: PROB_2  semantic presentation begin  





































theorem :: PROB_2:1 (Bool  "for" (Set (Var "r")) "," (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "r1"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "r3"))  ($#k10_real_1 :::"/"::: )  (Set (Var "r1")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r2"))  ($#k10_real_1 :::"/"::: )  (Set (Var "r")))) "iff" (Bool (Set (Set (Var "r3"))  ($#k8_real_1 :::"*"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r2"))  ($#k8_real_1 :::"*"::: )  (Set (Var "r1"))))  ")" )) ; 
 
theorem :: PROB_2:2 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "seq1")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq1")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq")) ")" )))  ")" ))) ; 
 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 "n" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); :: original: :::"."::: redefine func "ASeq" :::"."::: "n" ->    ($#m1_prob_1 :::"Event"::: )   "of" "Sigma"; end; 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")); func  :::"@Intersection"::: "ASeq" ->    ($#m1_prob_1 :::"Event"::: )   "of" "Sigma" equals :: PROB_2:def 1 (Set   ($#k3_prob_1 :::"Intersection"::: )  "ASeq"); end; 







:: deftheorem    defines :::"@Intersection"::: PROB_2:def 1 :  (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")) "holds"  (Bool (Set   ($#k2_prob_2 :::"@Intersection"::: )  (Set (Var "ASeq")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_prob_1 :::"Intersection"::: )  (Set (Var "ASeq"))))))); 
 
theorem :: PROB_2:3 (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 "B")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma")) (Bool  "ex" (Set (Var "BSeq")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) "st"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "BSeq"))  ($#k1_prob_2 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "ASeq"))  ($#k1_prob_2 :::"."::: )  (Set (Var "n")) ")" )  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B")))))))))) ; 
 
theorem :: PROB_2:4 (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")) "," (Set (Var "BSeq")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma"))  (Bool  "for" (Set (Var "B")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  "st" (Bool (Bool (Set (Var "ASeq")) "is"   ($#v2_prob_1 :::"non-ascending"::: )  ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "BSeq"))  ($#k1_prob_2 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "ASeq"))  ($#k1_prob_2 :::"."::: )  (Set (Var "n")) ")" )  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B"))))  ")" )) "holds"  (Bool (Set (Var "BSeq")) "is"   ($#v2_prob_1 :::"non-ascending"::: )  ))))) ; 
 
theorem :: PROB_2:5 (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 "BSeq")) "," (Set (Var "ASeq")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma"))  (Bool  "for" (Set (Var "B")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "BSeq"))  ($#k1_prob_2 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "ASeq"))  ($#k1_prob_2 :::"."::: )  (Set (Var "n")) ")" )  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B"))))  ")" )) "holds"  (Bool (Set (Set  "("  ($#k3_prob_1 :::"Intersection"::: )  (Set (Var "ASeq")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_prob_1 :::"Intersection"::: )  (Set (Var "BSeq")))))))) ; 
 registrationlet "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")); 
cluster (Set   ($#k2_prob_1 :::"Complement"::: )  "ASeq") -> "Sigma"  ($#v5_relat_1 :::"-valued"::: )   ; 
end; 
theorem :: PROB_2:6 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v2_prob_1 :::"non-ascending"::: )  ) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "S"))  ($#k1_prob_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "S"))  ($#k1_prob_2 :::"."::: )  (Set (Var "n")))))  ")" ))) ; 
 
theorem :: PROB_2:7 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v3_prob_1 :::"non-descending"::: )  ) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "S"))  ($#k1_prob_2 :::"."::: )  (Set (Var "n")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "S"))  ($#k1_prob_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))))  ")" ))) ; 
 
theorem :: PROB_2:8 (Bool  "for" (Set (Var "Omega")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "ASeq")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Omega")) "holds"   (Bool  "("  (Bool (Set (Var "ASeq")) "is"   ($#v2_prob_1 :::"non-ascending"::: )  ) "iff" (Bool (Set   ($#k2_prob_1 :::"Complement"::: )  (Set (Var "ASeq"))) "is"   ($#v3_prob_1 :::"non-descending"::: )  )  ")" ))) ; 
 definitionlet "F" be   ($#m1_hidden :::"Function":::); attr "F" is  :::"disjoint_valued":::  means :: PROB_2:def 2 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))) "holds"  (Bool (Set "F"  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_xboole_0 :::"misses"::: )  (Set "F"  ($#k1_funct_1 :::"."::: )  (Set (Var "y"))))); end; 




:: deftheorem    defines :::"disjoint_valued"::: PROB_2:def 2 :  (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v1_prob_2 :::"disjoint_valued"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))))  ")" )); 
 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")); :: original: :::"disjoint_valued"::: redefine attr "ASeq" is  :::"disjoint_valued":::  means :: PROB_2:def 3 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_hidden :::"<>"::: )  (Set (Var "n")))) "holds"  (Bool (Set "ASeq"  ($#k1_prob_2 :::"."::: )  (Set (Var "m")))  ($#r1_xboole_0 :::"misses"::: )  (Set "ASeq"  ($#k1_prob_2 :::"."::: )  (Set (Var "n"))))); end; 






:: deftheorem    defines :::"disjoint_valued"::: PROB_2:def 3 :  (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")) "holds"   (Bool  "("  (Bool (Set (Var "ASeq")) "is"   ($#v1_prob_2 :::"disjoint_valued"::: )  ) "iff" (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_hidden :::"<>"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "ASeq"))  ($#k1_prob_2 :::"."::: )  (Set (Var "m")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "ASeq"))  ($#k1_prob_2 :::"."::: )  (Set (Var "n")))))  ")" )))); 
 























theorem :: PROB_2:9 (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")) "," (Set (Var "P1")) "being"    ($#m2_prob_1 :::"Probability"::: )   "of" (Set (Var "Sigma"))  "st" (Bool (Bool  "("   "for" (Set (Var "A")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma")) "holds"  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "P1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A"))))  ")" )) "holds"  (Bool (Set (Var "P"))  ($#r2_funct_2 :::"="::: )  (Set (Var "P1")))))) ; 
 
theorem :: PROB_2:10 (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"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Sigma")) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "P")) "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 "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A"))))  ")" ) & (Bool (Set (Set (Var "P"))  ($#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 "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 (Var "B")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "ASeq")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma"))  "st" (Bool (Bool (Set (Var "ASeq")) "is"   ($#v3_prob_1 :::"non-descending"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set (Var "P"))  ($#k8_prob_1 :::"*"::: )  (Set (Var "ASeq"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "(" (Set (Var "P"))  ($#k8_prob_1 :::"*"::: )  (Set (Var "ASeq")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k1_prob_1 :::"Union"::: )  (Set (Var "ASeq")) ")" )))  ")" )  ")" )  ")" )  ")" )))) ; 
 
theorem :: PROB_2:11 (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")) "," (Set (Var "C")) "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  "(" (Set (Var "A"))  ($#k6_prob_1 :::"\/"::: )  (Set (Var "B")) ")" )  ($#k6_prob_1 :::"\/"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (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")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "C")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "B"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "C")) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "C")) ")" ) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B")) ")" )  ($#k5_prob_1 :::"/\"::: )  (Set (Var "C")) ")" ) ")" ))))))) ; 
 
theorem :: PROB_2:12 (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"))  ($#k7_prob_1 :::"\"::: )  (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B")) ")" ) ")" ))))))) ; 
 
theorem :: PROB_2:13 (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  "("  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")))) & (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A"))))  ")" ))))) ; 
 
theorem :: PROB_2:14 (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 "C")) "," (Set (Var "B")) "," (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"))  "st" (Bool (Bool (Set (Var "C"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "B"))  ($#k3_subset_1 :::"`"::: )  ))) "holds"  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "C")) ")" ) ")" ))))))) ; 
 
theorem :: PROB_2:15 (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  "(" (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 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B")) ")" ))))))) ; 
 
theorem :: PROB_2:16 (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_hidden :::"="::: )  (Set (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "("  ($#k4_prob_1 :::"[#]"::: )  (Set (Var "Sigma")) ")" )  ($#k7_prob_1 :::"\"::: )  (Set (Var "A")) ")" ) ")" ))))))) ; 
 
theorem :: PROB_2:17 (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  "("  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) "iff" (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "("  ($#k4_prob_1 :::"[#]"::: )  (Set (Var "Sigma")) ")" )  ($#k7_prob_1 :::"\"::: )  (Set (Var "A")) ")" )))  ")" ))))) ; 
 
theorem :: PROB_2:18 (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  "("  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "("  ($#k4_prob_1 :::"[#]"::: )  (Set (Var "Sigma")) ")" )  ($#k7_prob_1 :::"\"::: )  (Set (Var "A")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) "iff" (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A"))))  ")" ))))) ; 
 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")); let "P" be    ($#m2_prob_1 :::"Probability"::: )   "of" (Set (Const "Sigma")); let "A", "B" be    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Const "Sigma")); pred "A" "," "B" :::"are_independent_respect_to"::: "P" means :: PROB_2:def 4 (Bool (Set "P"  ($#k1_seq_1 :::"."::: )  (Set  "(" "A"  ($#k5_prob_1 :::"/\"::: )  "B" ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "P"  ($#k1_seq_1 :::"."::: )  "A" ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" "P"  ($#k1_seq_1 :::"."::: )  "B" ")" ))); let "C" be    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Const "Sigma")); pred "A" "," "B" "," "C" :::"are_independent_respect_to"::: "P" means :: PROB_2:def 5 (Bool  "("  (Bool (Set "P"  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "(" "A"  ($#k5_prob_1 :::"/\"::: )  "B" ")" )  ($#k5_prob_1 :::"/\"::: )  "C" ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" "P"  ($#k1_seq_1 :::"."::: )  "A" ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" "P"  ($#k1_seq_1 :::"."::: )  "B" ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" "P"  ($#k1_seq_1 :::"."::: )  "C" ")" ))) & (Bool (Set "P"  ($#k1_seq_1 :::"."::: )  (Set  "(" "A"  ($#k5_prob_1 :::"/\"::: )  "B" ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "P"  ($#k1_seq_1 :::"."::: )  "A" ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" "P"  ($#k1_seq_1 :::"."::: )  "B" ")" ))) & (Bool (Set "P"  ($#k1_seq_1 :::"."::: )  (Set  "(" "A"  ($#k5_prob_1 :::"/\"::: )  "C" ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "P"  ($#k1_seq_1 :::"."::: )  "A" ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" "P"  ($#k1_seq_1 :::"."::: )  "C" ")" ))) & (Bool (Set "P"  ($#k1_seq_1 :::"."::: )  (Set  "(" "B"  ($#k5_prob_1 :::"/\"::: )  "C" ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "P"  ($#k1_seq_1 :::"."::: )  "B" ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" "P"  ($#k1_seq_1 :::"."::: )  "C" ")" )))  ")" ); end; 

















:: deftheorem    defines :::"are_independent_respect_to"::: PROB_2:def 4 :  (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"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma")) "holds"   (Bool  "("  (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r1_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P"))) "iff" (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )))  ")" ))))); 
 
:: deftheorem    defines :::"are_independent_respect_to"::: PROB_2:def 5 :  (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"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma")) "holds"   (Bool  "("  (Bool (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C"))  ($#r2_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P"))) "iff" (Bool  "("  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B")) ")" )  ($#k5_prob_1 :::"/\"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "C")) ")" ))) & (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" ))) & (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "C")) ")" ))) & (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "B"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "C")) ")" )))  ")" )  ")" ))))); 
 
theorem :: PROB_2:19 (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")) "," (Set (Var "B"))  ($#r1_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "B")) "," (Set (Var "A"))  ($#r1_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P"))))))) ; 
 
theorem :: PROB_2:20 (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")) "," (Set (Var "C")) "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  "("  (Bool (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C"))  ($#r2_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P"))) "iff" (Bool  "("  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B")) ")" )  ($#k5_prob_1 :::"/\"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "C")) ")" ))) & (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r1_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P"))) & (Bool (Set (Var "B")) "," (Set (Var "C"))  ($#r1_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P"))) & (Bool (Set (Var "A")) "," (Set (Var "C"))  ($#r1_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P")))  ")" )  ")" ))))) ; 
 
theorem :: PROB_2:21 (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")) "," (Set (Var "C")) "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")) "," (Set (Var "B")) "," (Set (Var "C"))  ($#r2_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "B")) "," (Set (Var "A")) "," (Set (Var "C"))  ($#r2_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P"))))))) ; 
 
theorem :: PROB_2:22 (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")) "," (Set (Var "C")) "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")) "," (Set (Var "B")) "," (Set (Var "C"))  ($#r2_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "B"))  ($#r2_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P"))))))) ; 
 
theorem :: PROB_2:23 (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"))  (Bool  "for" (Set (Var "E")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  "st" (Bool (Bool (Set (Var "E"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Var "A")) "," (Set (Var "E"))  ($#r1_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P")))))))) ; 
 
theorem :: PROB_2:24 (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 (Var "A")) "," (Set   ($#k4_prob_1 :::"[#]"::: )  (Set (Var "Sigma")))  ($#r1_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P"))))))) ; 
 
theorem :: PROB_2:25 (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")) "," (Set (Var "B"))  ($#r1_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "A")) "," (Set (Set  "("  ($#k4_prob_1 :::"[#]"::: )  (Set (Var "Sigma")) ")" )  ($#k7_prob_1 :::"\"::: )  (Set (Var "B")))  ($#r1_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P"))))))) ; 
 
theorem :: PROB_2:26 (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")) "," (Set (Var "B"))  ($#r1_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Set  "("  ($#k4_prob_1 :::"[#]"::: )  (Set (Var "Sigma")) ")" )  ($#k7_prob_1 :::"\"::: )  (Set (Var "A"))) "," (Set (Set  "("  ($#k4_prob_1 :::"[#]"::: )  (Set (Var "Sigma")) ")" )  ($#k7_prob_1 :::"\"::: )  (Set (Var "B")))  ($#r1_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P"))))))) ; 
 
theorem :: PROB_2:27 (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")) "," (Set (Var "C")) "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")) "," (Set (Var "B"))  ($#r1_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P"))) & (Bool (Set (Var "A")) "," (Set (Var "C"))  ($#r1_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P"))) & (Bool (Set (Var "B"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "C")))) "holds"  (Bool (Set (Var "A")) "," (Set (Set (Var "B"))  ($#k6_prob_1 :::"\/"::: )  (Set (Var "C")))  ($#r1_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P"))))))) ; 
 
theorem :: PROB_2:28 (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"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r1_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P"))) & (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k6_prob_1 :::"\/"::: )  (Set (Var "B")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)))))) ; 
 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")); let "P" be    ($#m2_prob_1 :::"Probability"::: )   "of" (Set (Const "Sigma")); let "B" be    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Const "Sigma")); assume 
(Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Const "P"))  ($#k1_seq_1 :::"."::: )  (Set (Const "B"))))
 ; func "P" :::".|."::: "B" ->    ($#m2_prob_1 :::"Probability"::: )   "of" "Sigma" means :: PROB_2:def 6 (Bool  "for" (Set (Var "A")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" "Sigma" "holds"  (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "P"  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  "B" ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" "P"  ($#k1_seq_1 :::"."::: )  "B" ")" )))); end; 









:: deftheorem    defines :::".|."::: PROB_2:def 6 :  (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"))  (Bool  "for" (Set (Var "B")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B"))))) "holds"  (Bool  "for" (Set (Var "b5")) "being"    ($#m2_prob_1 :::"Probability"::: )   "of" (Set (Var "Sigma")) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "B")))) "iff" (Bool  "for" (Set (Var "A")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma")) "holds"  (Bool (Set (Set (Var "b5"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" ))))  ")" )))))); 
 
theorem :: PROB_2:29 (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"))  (Bool  "for" (Set (Var "B")) "," (Set (Var "A")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "B")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" ))))))) ; 
 
theorem :: PROB_2: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"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B")) ")" )))) "holds"  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B")) ")" )  ($#k5_prob_1 :::"/\"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set  "(" (Set (Var "A"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "B")) ")" ) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "C")) ")" ))))))) ; 
 
theorem :: PROB_2: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 "P")) "being"    ($#m2_prob_1 :::"Probability"::: )   "of" (Set (Var "Sigma"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  "st" (Bool (Bool (Set (Var "C"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "B"))  ($#k3_subset_1 :::"`"::: )  )) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "C"))))) "holds"  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "B")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "C")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "C")) ")" ) ")" ))))))) ; 
 
theorem :: PROB_2: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 "P")) "being"    ($#m2_prob_1 :::"Probability"::: )   "of" (Set (Var "Sigma"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  "st" (Bool (Bool (Set (Var "A1"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "A2"))) & (Bool (Set (Var "A3"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A1"))  ($#k6_prob_1 :::"\/"::: )  (Set (Var "A2")) ")" )  ($#k3_subset_1 :::"`"::: )  )) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A1")))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A2")))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A3"))))) "holds"  (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A1")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A2")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A2")) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A3")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A3")) ")" ) ")" ))))))) ; 
 
theorem :: PROB_2: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 "P")) "being"    ($#m2_prob_1 :::"Probability"::: )   "of" (Set (Var "Sigma"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B"))))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "B")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")))) "iff" (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r1_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P")))  ")" ))))) ; 
 
theorem :: PROB_2: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 "P")) "being"    ($#m2_prob_1 :::"Probability"::: )   "of" (Set (Var "Sigma"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")))) & (Bool (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "B")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set  "(" (Set  "("  ($#k4_prob_1 :::"[#]"::: )  (Set (Var "Sigma")) ")" )  ($#k7_prob_1 :::"\"::: )  (Set (Var "B")) ")" ) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r1_prob_2 :::"are_independent_respect_to"::: )  (Set (Var "P"))))))) ; 
 
theorem :: PROB_2: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 "P")) "being"    ($#m2_prob_1 :::"Probability"::: )   "of" (Set (Var "Sigma"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_prob_1 :::"Event"::: )   "of" (Set (Var "Sigma"))  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B"))))) "holds"  (Bool (Set (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 :::"-"::: )  (Num 1) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "B")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "A")))))))) ; 
 
theorem :: PROB_2: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"))  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "B")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" ))))))) ; 
 
theorem :: PROB_2: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 "B")) "," (Set (Var "A1")) "," (Set (Var "A2")) "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   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")))) & (Bool (Set (Var "A2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A1"))  ($#k3_subset_1 :::"`"::: )  )) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A1")))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A2"))))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "B")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "A1")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A1")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A1")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A2")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A2")) ")" ) ")" ) ")" ))) & (Bool (Set (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "B")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "A2")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A2")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A2")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A1")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A2")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A2")) ")" ) ")" ) ")" )))  ")" ))))) ; 
 
theorem :: PROB_2: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 "B")) "," (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) "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   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A1")))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A2")))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A3")))) & (Bool (Set (Var "A1"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "A2"))) & (Bool (Set (Var "A3"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A1"))  ($#k6_prob_1 :::"\/"::: )  (Set (Var "A2")) ")" )  ($#k3_subset_1 :::"`"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "B")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "A1")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A1")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A1")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A2")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A2")) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A3")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A3")) ")" ) ")" ) ")" ))) & (Bool (Set (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "B")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "A2")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A2")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A2")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A1")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A2")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A2")) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A3")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A3")) ")" ) ")" ) ")" ))) & (Bool (Set (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "B")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "A3")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A3")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A3")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A1")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A2")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A2")) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "A3")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "A3")) ")" ) ")" ) ")" )))  ")" ))))) ; 
 
theorem :: PROB_2: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"))  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "("  ($#k4_prob_1 :::"[#]"::: )  (Set (Var "Sigma")) ")" )  ($#k7_prob_1 :::"\"::: )  (Set (Var "A")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "B")) ")" ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "P"))  ($#k3_prob_2 :::".|."::: )  (Set (Var "B")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "A")))))))) ;