for X being non empty set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for m being induced_Measure of S,P
for M being induced_sigma_Measure of S,m holds M is_extension_of m