begin
theorem
canceled;
theorem
canceled;
theorem Th3:
:: deftheorem Def1 defines compl-closed PROB_1:def 1 :
theorem Th4:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
Lm1:
for X being set
for A1 being SetSequence of X
for n being Element of NAT holds A1 . n in bool X
;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th23:
theorem
canceled;
theorem Th25:
theorem Th26:
:: deftheorem PROB_1:def 2 :
canceled;
:: deftheorem PROB_1:def 3 :
canceled;
:: deftheorem Def4 defines Complement PROB_1:def 4 :
:: deftheorem defines Intersection PROB_1:def 5 :
theorem
canceled;
theorem
canceled;
theorem Th29:
Lm2:
for X being set
for A, B being Subset of holds Complement (A followed_by B) = (A ` ) followed_by (B ` )
theorem Th30:
:: deftheorem Def6 defines non-ascending PROB_1:def 6 :
:: deftheorem defines non-descending PROB_1:def 7 :
:: deftheorem Def8 defines sigma-multiplicative PROB_1:def 8 :
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem Th35:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th46:
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem PROB_1:def 9 :
canceled;
:: deftheorem PROB_1:def 10 :
canceled;
:: deftheorem defines [#] PROB_1:def 11 :
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem Th59:
theorem Th60:
theorem
canceled;
theorem Th62:
:: deftheorem PROB_1:def 12 :
canceled;
:: deftheorem Def13 defines Probability PROB_1:def 13 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th67:
theorem
theorem Th69:
theorem Th70:
theorem
theorem Th72:
theorem Th73:
theorem Th74:
theorem
theorem Th76:
Lm3:
for Omega being non empty set
for X being Subset-Family of ex Y being SigmaField of Omega st
( X c= Y & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
Y c= Z ) )
:: deftheorem defines sigma PROB_1:def 14 :
:: deftheorem defines halfline PROB_1:def 15 :
:: deftheorem defines Family_of_halflines PROB_1:def 16 :
:: deftheorem defines Borel_Sets PROB_1:def 17 :
theorem