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