let I be I_Lattice; :: thesis: for FI being Filter of I st I is lower-bounded holds
( I /\/ FI is 0_Lattice & Bottom (I /\/ FI) = (Bottom I) /\/ FI )
let FI be Filter of I; :: thesis: ( I is lower-bounded implies ( I /\/ FI is 0_Lattice & Bottom (I /\/ FI) = (Bottom I) /\/ FI ) )
assume A1: I is lower-bounded ; :: thesis: ( I /\/ FI is 0_Lattice & Bottom (I /\/ FI) = (Bottom I) /\/ FI )
then consider i being Element of I such that
A2: for j being Element of I holds
( i "/\" j = i & j "/\" i = i ) by LATTICES:def 13;
A3: Bottom I = i by A1, A2, LATTICES:def 16;
set L = I /\/ FI;
set R = equivalence_wrt FI;
set x = i /\/ FI;

A4: now

let y be Element of (I /\/ FI); :: thesis: ( (i /\/ FI) "/\" y = i /\/ FI & y "/\" (i /\/ FI) = i /\/ FI )
I /\/ FI = LattStr(# (Class (equivalence_wrt FI)),(the L_join of I /\/ (equivalence_wrt FI)),(the L_meet of I /\/ (equivalence_wrt FI)) #) by Def5;
then consider j being Element of I such that
A5: y = Class (equivalence_wrt FI),j by EQREL_1:45;
A6: ( i "/\" j = i & y = j /\/ FI ) by A2, A5, Def6;
hence (i /\/ FI) "/\" y = i /\/ FI by Th15; :: thesis: y "/\" (i /\/ FI) = i /\/ FI
thus y "/\" (i /\/ FI) = i /\/ FI by A6, Th15; :: thesis: verum

end;

hence I /\/ FI is 0_Lattice by LATTICES:def 13; :: thesis: Bottom (I /\/ FI) = (Bottom I) /\/ FI
hence Bottom (I /\/ FI) = (Bottom I) /\/ FI by A3, A4, LATTICES:def 16; :: thesis: verum