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 ) )
set L = I /\/ FI;
set R = equivalence_wrt 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 ) ;
set x = i /\/ FI;

A3: now :: thesis: for y being Element of (I /\/ FI) holds
( (i /\/ FI) "/\" y = i /\/ FI & y "/\" (i /\/ FI) = i /\/ FI )

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
A4: y = Class ((equivalence_wrt FI),j) by EQREL_1:36;
A5: i "/\" j = i by A2;
A6: y = j /\/ FI by A4, Def6;
hence (i /\/ FI) "/\" y = i /\/ FI by A5, Th15; :: thesis: y "/\" (i /\/ FI) = i /\/ FI
thus y "/\" (i /\/ FI) = i /\/ FI by A5, A6, Th15; :: thesis: verum

end;

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