begin
Lm1:
for X being set
for A, B being Subset of X holds Complement (A followed_by B) = (A `) followed_by (B `)
theorem Th27:
for
Omega,
p being
set for
Sigma being
SigmaField of
Omega ex
f being
Function st
(
dom f = Sigma & ( for
D being
Subset of
Omega st
D in Sigma holds
( (
p in D implies
f . D = 1 ) & ( not
p in D implies
f . D = 0 ) ) ) )
theorem Th28:
for
Omega,
p being
set for
Sigma being
SigmaField of
Omega ex
P being
Function of
Sigma,
REAL st
for
D being
Subset of
Omega st
D in Sigma holds
( (
p in D implies
P . D = 1 ) & ( not
p in D implies
P . D = 0 ) )
:: a field of subsets of given nonempty set Omega. ::