theorem Th30: :: FILTER_0:30

for I being I_Lattice
for i, j being Element of I
for FI being Filter of I st j in FI holds
i => j in FI