let Omega be non empty set ; :: thesis: for A, B being Subset of Omega
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds
A \/ B in D
let A, B be Subset of Omega; :: thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds
A \/ B in D
let D be non empty Subset-Family of Omega; :: thesis: ( D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D implies A \/ B in D )
assume that
A1: D is Dynkin_System of Omega and
A2: D is intersection_stable ; :: thesis: ( not A in D or not B in D or A \/ B in D )
assume ( A in D & B in D ) ; :: thesis: A \/ B in D
then ( A ` in D & B ` in D ) by A1, Def5;
then (A `) /\ (B `) in D by A2, FINSUB_1:def 2;
then (A \/ B) ` in D by XBOOLE_1:53;
then ((A \/ B) `) ` in D by A1, Def5;
hence A \/ B in D ; :: thesis: verum