let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; :: thesis: L is complemented
for b being Element of L ex a being Element of L st a is_a_complement_of b

proof

let b be Element of L; :: thesis: ex a being Element of L st a is_a_complement_of b
consider a being Element of L such that
A1: a is_a_complement'_of b by Def7;
b "/\" a = Bot' L by A1, Def6;
then A2: b "/\" a = Bottom L by Th20;
b "\/" a = Top' L by A1, Def6;
then b "\/" a = Top L by Th19;
then a is_a_complement_of b by A2, LATTICES:def 18;
hence ex a being Element of L st a is_a_complement_of b ; :: thesis: verum

end;

hence L is complemented by LATTICES:def 19; :: thesis: verum