let I1, I2 be Dynkin_System of Omega; :: thesis: ( E c= I1 & ( for D being Dynkin_System of Omega st E c= D holds
I1 c= D ) & E c= I2 & ( for D being Dynkin_System of Omega st E c= D holds
I2 c= D ) implies I1 = I2 )
assume A2: ( E c= I1 & ( for D being Dynkin_System of Omega st E c= D holds
I1 c= D ) ) ; :: thesis: ( not E c= I2 or ex D being Dynkin_System of Omega st
( E c= D & not I2 c= D ) or I1 = I2 )
assume ( E c= I2 & ( for D being Dynkin_System of Omega st E c= D holds
I2 c= D ) ) ; :: thesis: I1 = I2
then ( I1 c= I2 & I2 c= I1 ) by A2;
hence I1 = I2 by XBOOLE_0:def 10; :: thesis: verum