let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; :: thesis: L is upper-bounded
ex c being Element of L st
for a being Element of L holds
( c "\/" a = c & a "\/" c = c )

proof

take Top' L ; :: thesis: for a being Element of L holds
( (Top' L) "\/" a = Top' L & a "\/" (Top' L) = Top' L )
let a be Element of L; :: thesis: ( (Top' L) "\/" a = Top' L & a "\/" (Top' L) = Top' L )
thus ( (Top' L) "\/" a = Top' L & a "\/" (Top' L) = Top' L ) by Th4; :: thesis: verum

end;

hence L is upper-bounded ; :: thesis: verum