P
.
n
is
Probability
of
(
Trivial-SigmaField_sequence
D
)
.
n
;
hence
P
.
n
is
Probability
of
Trivial-SigmaField
(
D
.
n
)
by
Def12
;
:: thesis:
verum