let I be I_Lattice; :: thesis:
let FI be Filter of I; :: thesis:
set L = I /\/ FI;
set R = equivalence_wrt FI;
assume A1: I is lower-bounded ; :: thesis:
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:

let y be Element of (I /\/ FI); :: thesis:
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:
thus y "/\" (i /\/ FI) = i /\/ FI by A5, A6, Th15; :: thesis:

end;

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