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) = () /\/ FI )

let FI be Filter of I; :: thesis: ( I is lower-bounded implies ( I /\/ FI is 0_Lattice & Bottom (I /\/ FI) = () /\/ 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) = () /\/ 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 ()),( the L_join of I /\/ ()),( the L_meet of I /\/ ()) #) by Def5;
then consider j being Element of I such that
A4: y = Class ((),j) by EQREL_1:36;
A5: i "/\" j = i by A2;
A6: y = j /\/ FI by ;
hence (i /\/ FI) "/\" y = i /\/ FI by ; :: 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) = () /\/ FI
Bottom I = i by ;
hence Bottom (I /\/ FI) = () /\/ FI by ; :: thesis: verum