let L be bounded Lattice; :: thesis: for a being Element of L holds Bottom L in PseudoComplements a
let a be Element of L; :: thesis: Bottom L in PseudoComplements a
a "/\" (Bottom L) = Bottom L ;
hence Bottom L in PseudoComplements a ; :: thesis: verum