let A, B, X be set ; :: thesis: for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds
A /\ B in sigma_Field C
let C be C_Measure of X; :: thesis: ( A in sigma_Field C & B in sigma_Field C implies A /\ B in sigma_Field C )
assume that
A1: A in sigma_Field C and
A2: B in sigma_Field C ; :: thesis: A /\ B in sigma_Field C
A3: X \ B in sigma_Field C by A2, Th7;
A /\ B c= X /\ X by A1, A2, XBOOLE_1:27;
then A4: A /\ B = X /\ (A /\ B) by XBOOLE_1:28
.= X \ (X \ (A /\ B)) by XBOOLE_1:48
.= X \ ((X \ A) \/ (X \ B)) by XBOOLE_1:54 ;
X \ A in sigma_Field C by A1, Th7;
then (X \ A) \/ (X \ B) in sigma_Field C by A3, Th8;
hence A /\ B in sigma_Field C by A4, Th7; :: thesis: verum