let L be Lattice; :: thesis: 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; :: thesis: ( L is B_Lattice & p [= q implies latt (L,[#p,q#]) is B_Lattice )
assume ( L is B_Lattice & p [= q ) ; :: thesis: 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 ; :: thesis: verum