theorem Th16: :: FILTER_1:16

for I being I_Lattice
for FI being Filter of I
for i, j being Element of I holds
( i /\/ FI [= j /\/ FI iff i => j in FI )