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 Def5;
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 sequence of 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 Th7;
then Union r in D by A1, Def5;
hence x \/ y in D by Th2; :: thesis: verum