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

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

thus
B /\/ FB is B_Lattice
by A4; :: thesis: verum
let x be Element of L; :: according to LATTICES:def 19 :: thesis: ex b_{1} being Element of the carrier of L st b_{1} 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;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