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;

Bottom I = i by A1, A2, LATTICES:def 16;

hence Bottom (I /\/ FI) = (Bottom I) /\/ FI by A3, A7, LATTICES:def 16; :: thesis: verum

( 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 )

hence A7:
I /\/ FI is 0_Lattice
by LATTICES:def 13; :: thesis: Bottom (I /\/ FI) = (Bottom I) /\/ FI( (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;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

Bottom I = i by A1, A2, LATTICES:def 16;

hence Bottom (I /\/ FI) = (Bottom I) /\/ FI by A3, A7, LATTICES:def 16; :: thesis: verum