let Omega be non empty set ; :: thesis: for D being Dynkin_System of Omega
for x, y being Element of D st x c= y holds
y \ x in D
let D be Dynkin_System of Omega; :: thesis: for x, y being Element of D st x c= y holds
y \ x in D
let x, y be Element of D; :: thesis: ( x c= y implies y \ x in D )
assume A1: x c= y ; :: thesis: y \ x in D
A2: y ` in D by Def7;
x c= (y ` ) ` by A1;
then x misses y ` by SUBSET_1:43;
then A3: x \/ (y ` ) in D by A2, Th21;
(x \/ (y ` )) ` = (x ` ) /\ ((y ` ) ` ) by XBOOLE_1:53
.= y \ x by SUBSET_1:32 ;
hence y \ x in D by A3, Def7; :: thesis: verum