begin
theorem Th1:
theorem Th2:
for
r being
Real holds
( not
r * r = r or
r = 0 or
r = 1 )
theorem Th3:
:: deftheorem Def1 defines Indep KOLMOG01:def 1 :
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
:: deftheorem Def2 defines ManySortedSigmaField KOLMOG01:def 2 :
:: deftheorem Def3 defines is_independent_wrt KOLMOG01:def 3 :
:: deftheorem Def4 defines SigmaSection KOLMOG01:def 4 :
:: deftheorem Def5 defines is_independent_wrt KOLMOG01:def 5 :
:: deftheorem defines sigUn KOLMOG01:def 6 :
:: deftheorem Def7 defines futSigmaFields KOLMOG01:def 7 :
:: deftheorem defines tailSigmaField KOLMOG01:def 8 :
:: deftheorem Def9 defines MeetSections KOLMOG01:def 9 :
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
:: deftheorem Def10 defines finSigmaFields KOLMOG01:def 10 :
theorem Th15:
theorem