for I being I_Lattice
for FI being Filter of I st I is lower-bounded holds
( I /\/ FI is 0_Lattice & Bottom (I /\/ FI) = (Bottom I) /\/ FI )