reconsider M = P --> 0. as Function of P,ExtREAL ;
take M ; :: thesis: ( M is nonnegative & M is additive & M is zeroed )
thus ( M is nonnegative & M is additive & M is zeroed ) by LM; :: thesis: verum