for I being I_Lattice
for FI being Filter of I holds
( I /\/ FI is 1_Lattice & Top (I /\/ FI) = (Top I) /\/ FI )