let L be B_Lattice; :: thesis: for a being Element of L holds (a `) "\/" a = Top L
let a be Element of L; :: thesis: (a `) "\/" a = Top L
a ` is_a_complement_of a by Def21;
hence (a `) "\/" a = Top L ; :: thesis: verum