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