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;
A2: B /\/ FB is 0_Lattice by Th18;
A4: Bottom (B /\/ FB) = (Bottom B) /\/ FB by Th18;
A5: Top (B /\/ FB) = (Top B) /\/ FB by Th19;
reconsider L = B /\/ FB as 01_Lattice by A2;
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 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 A7, Def6;
hence y "\/" x = ((a `) "\/" a) /\/ FB by 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 A8, Th15
.= Bottom L by A4, LATTICES:47 ; :: thesis: x "/\" y = Bottom L
hence x "/\" y = Bottom L ; :: thesis: verum

end;

thus B /\/ FB is B_Lattice by A6; :: thesis: verum