let
A
be
Event
of
Borel_Sets
;
:: thesis:
0
<=
P
.
A
now
:: thesis:
0
<=
P
.
A
per
cases
(
0
in
A
or not
0
in
A
)
;
suppose
0
in
A
;
:: thesis:
0
<=
P
.
A
then
P
.
A
=
1
by
Lm1
;
hence
0
<=
P
.
A
;
:: thesis:
verum
end;
suppose
not
0
in
A
;
:: thesis:
0
<=
P
.
A
hence
0
<=
P
.
A
by
Lm1
;
:: thesis:
verum
end;
end;
end;
hence
0
<=
P
.
A
;
:: thesis:
verum