let B be B_Lattice; :: thesis: for FB being Filter of B holds B /\/ FB is B_Lattice
let FB be Filter of B; :: thesis: B /\/ FB is B_Lattice
set L = B /\/ FB;
set R = equivalence_wrt FB;
A1: B is I_Lattice by FILTER_0:40;
then A2: B /\/ FB is 0_Lattice by Th18;
A3: B /\/ FB is 1_Lattice by A1, Th19;
A4: Bottom (B /\/ FB) = (Bottom B) /\/ FB by A1, Th18;
A5: Top (B /\/ FB) = (Top B) /\/ FB by A1, Th19;
reconsider L = B /\/ FB as 01_Lattice by A2, A3;
A6: L is complemented

proof

let x be Element of L; :: according to LATTICES:def 19 :: thesis: ex b₁ being Element of the carrier of L st b₁ is_a_complement_of x
L = LattStr(# (Class (equivalence_wrt FB)),(the L_join of B /\/ (equivalence_wrt FB)),(the L_meet of B /\/ (equivalence_wrt FB)) #) by A1, Def5;
then consider a being Element of B such that
A7: x = Class (equivalence_wrt FB),a by EQREL_1:45;
reconsider y = (a ` ) /\/ FB as Element of L ;
take y ; :: thesis: y is_a_complement_of x
A8: x = a /\/ FB by A1, A7, Def6;
hence y "\/" x = ((a ` ) "\/" a) /\/ FB by A1, Th15
.= Top L by A5, LATTICES:48 ;
:: according to LATTICES:def 18 :: thesis: ( x "\/" y = Top L & y "/\" x = Bottom L & x "/\" y = Bottom L )
hence x "\/" y = Top L ; :: thesis: ( y "/\" x = Bottom L & x "/\" y = Bottom L )
thus y "/\" x = ((a ` ) "/\" a) /\/ FB by A1, A8, Th15
.= Bottom L by A4, LATTICES:47 ; :: thesis: x "/\" y = Bottom L
hence x "/\" y = Bottom L ; :: thesis: verum

end;

L is I_Lattice by A1, Th20;
hence B /\/ FB is B_Lattice by A6; :: thesis: verum