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 )
A1: (x \/ (y `)) ` = (x `) /\ ((y `) `) by XBOOLE_1:53
.= y \ x by SUBSET_1:13 ;
assume x c= y ; :: thesis: y \ x in D
then x c= (y `) ` ;
then A2: x misses y ` by SUBSET_1:23;
y ` in D by Def5;
then x \/ (y `) in D by A2, Th17;
hence y \ x in D by A1, Def5; :: thesis: verum