let X, A, B 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 A1: ( A in sigma_Field C & B in sigma_Field C ) ; :: thesis: A /\ B in sigma_Field C
then A /\ B c= X /\ X by XBOOLE_1:27;
then A2: 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 & X \ B in sigma_Field C ) by A1, Th16;
then (X \ A) \/ (X \ B) in sigma_Field C by Th17;
hence A /\ B in sigma_Field C by A2, Th16; :: thesis: verum