theorem Th40: :: FILTER_0:40

for I being I_Lattice
for i, j being Element of I
for DI being non empty Subset of I st j in <.(DI \/ {i}).) holds
i => j in <.DI.)