let L be non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' LattStr ; :: thesis: for x being Element of L holds x "\/" (x `#) = Top' L
let x be Element of L; :: thesis: x "\/" (x `#) = Top' L
x `# is_a_complement'_of x by Def8;
hence x "\/" (x `#) = Top' L ; :: thesis: verum