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