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 Th78, Th86;
hence latt L,[#p,q#] is B_Lattice ; :: thesis: verum