let X be set ; :: thesis: for C being C_Measure of X holds sigma_Meas C is complete
let C be C_Measure of X; :: thesis: sigma_Meas C is complete
let A be Subset of X; :: according to MEASURE3:def 1 :: thesis: for b₁ being set holds
( not b₁ in sigma_Field C or not A c= b₁ or not (sigma_Meas C) . b₁ = 0. or A in sigma_Field C )
let B be set ; :: thesis: ( not B in sigma_Field C or not A c= B or not (sigma_Meas C) . B = 0. or A in sigma_Field C )
assume that
A1: B in sigma_Field C and
A2: A c= B and
A3: (sigma_Meas C) . B = 0. ; :: thesis: A in sigma_Field C
reconsider B = B as Subset of X by A1;
C is V92() by Def1;
then A4: 0. <= C . A by MEASURE1:def 2;
C . B = 0. by A1, A3, Def3;
then C . A = 0. by A2, A4, Def1;
hence A in sigma_Field C by Th15; :: thesis: verum