let L be Lattice; for p, q being Element of L st L is B_Lattice & p [= q holds
latt (L,[#p,q#]) is B_Lattice
let p, q be Element of L; ( L is B_Lattice & p [= q implies latt (L,[#p,q#]) is B_Lattice )
assume
( L is B_Lattice & p [= q )
; latt (L,[#p,q#]) is B_Lattice
then
latt (L,[#p,q#]) is distributive bounded complemented Lattice
by Th77, Th84;
hence
latt (L,[#p,q#]) is B_Lattice
; verum