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 that
A3: A in D and
A4: B in D ; :: thesis: A \ B in D
B ` in D by A1, A4, Def5;
then A /\ (B `) in D by A2, A3, FINSUB_1:def 2;
hence A \ B in D by SUBSET_1:13; :: thesis: verum