let Omega be non empty set ; :: thesis: for D being Dynkin_System of Omega
for x, y being Element of D st x misses y holds
x \/ y in D
let D be Dynkin_System of Omega; :: thesis: for x, y being Element of D st x misses y holds
x \/ y in D
reconsider e = {} as Element of D by Def7;
let x, y be Element of D; :: thesis: ( x misses y implies x \/ y in D )
reconsider x1 = x as Subset of Omega ;
reconsider y1 = y as Subset of Omega ;
reconsider r = x1,y1 followed_by ({} Omega) as SetSequence of Omega ;
x,y followed_by e is Function of NAT ,D by Lm1;
then A1: rng r c= D by RELAT_1:def 19;
assume x misses y ; :: thesis: x \/ y in D
then r is disjoint_valued by Th11;
then Union r in D by A1, Def7;
hence x \/ y in D by Th6; :: thesis: verum