begin
theorem Th1:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
scheme
DomsetFamEx{
F1()
-> set ,
P1[
set ] } :
provided
A1:
ex
B being
set st
(
B c= F1() &
P1[
B] )
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th15:
:: deftheorem MEASURE1:def 1 :
canceled;
:: deftheorem MEASURE1:def 2 :
canceled;
:: deftheorem Def3 defines compl-closed MEASURE1:def 3 :
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem Th20:
theorem
:: deftheorem Def4 defines nonnegative MEASURE1:def 4 :
theorem
canceled;
theorem
canceled;
:: deftheorem Def5 defines additive MEASURE1:def 5 :
theorem
canceled;
theorem Th25:
theorem Th26:
theorem Th27:
theorem
canceled;
theorem
:: deftheorem MEASURE1:def 6 :
canceled;
:: deftheorem Def7 defines measure_zero MEASURE1:def 7 :
theorem
canceled;
theorem
theorem
theorem
theorem Th34:
theorem Th35:
theorem
canceled;
theorem
canceled;
theorem Th38:
theorem
theorem Th40:
theorem
theorem Th42:
:: deftheorem MEASURE1:def 8 :
canceled;
:: deftheorem Def9 defines sigma-additive MEASURE1:def 9 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th49:
theorem
canceled;
theorem
canceled;
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem
theorem Th57:
:: deftheorem MEASURE1:def 10 :
canceled;
:: deftheorem Def11 defines sigma-additive MEASURE1:def 11 :
theorem
canceled;
theorem
canceled;
theorem Th60:
theorem
theorem Th62:
theorem
theorem Th64:
theorem
canceled;
theorem
theorem
:: deftheorem MEASURE1:def 12 :
canceled;
:: deftheorem Def13 defines measure_zero MEASURE1:def 13 :
theorem
canceled;
theorem
theorem
theorem