let L be non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ; :: thesis: L is upper-bounded
consider c being Element of L such that
A1: for a being Element of L holds
( c + a = c & a + (a `) = c ) by Th5;
for a being Element of L holds
( a + c = c & a + (a `) = c ) by A1;
hence L is upper-bounded by A1; :: thesis: verum