let X, S be set ; :: thesis: ( S is SigmaField of X implies S is SigmaRing of X )
assume A1: S is SigmaField of X ; :: thesis: S is SigmaRing of X
then for F being SetSequence of X st rng F c= S holds
Union F in S by PROB_4:4;
hence S is SigmaRing of X by A1, DefSigmaRing; :: thesis: verum