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 c = Top' L; :: thesis: for a being Element of L holds
( c "\/" a = c & a "\/" c = c )
let a be Element of L; :: thesis: ( c "\/" a = c & a "\/" c = c )
thus ( c "\/" a = c & a "\/" c = c ) by Th5; :: thesis: verum

end;

hence L is upper-bounded by LATTICES:def 14; :: thesis: verum