let L be Lattice; :: thesis: for p being Element of L st L is B_Lattice holds
latt <.p.) is B_Lattice
let p be Element of L; :: thesis: ( L is B_Lattice implies latt <.p.) is B_Lattice )
assume L is B_Lattice ; :: thesis: latt <.p.) is B_Lattice
then latt <.p.) is distributive bounded complemented Lattice by Th54, Th59;
hence latt <.p.) is B_Lattice ; :: thesis: verum