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 /\/ FB is 0_Lattice by Th18;
A2: Bottom (B /\/ FB) = (Bottom B) /\/ FB by Th18;
A3: Top (B /\/ FB) = (Top B) /\/ FB by Th19;
reconsider L = B /\/ FB as 01_Lattice by A1;
A4: L is complemented
proof
let x be Element of L; :: according to LATTICES:def 19 :: thesis: ex b1 being Element of the carrier of L st b1 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
A5: x = Class ((equivalence_wrt FB),a) by EQREL_1:36;
reconsider y = (a `) /\/ FB as Element of L ;
take y ; :: thesis: y is_a_complement_of x
A6: x = a /\/ FB by A5, Def6;
hence y "\/" x = ((a `) "\/" a) /\/ FB by Th15
.= (Top B) /\/ FB by LATTICES:21
.= Top L by A3 ;
:: 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 A6, Th15
.= Bottom L by A2, LATTICES:20 ; :: thesis: x "/\" y = Bottom L
hence x "/\" y = Bottom L ; :: thesis: verum
end;
thus B /\/ FB is B_Lattice by A4; :: thesis: verum