let L be non empty Lattice-like Boolean upper-bounded' lower-bounded' distributive' 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 LATTICES:def 19;
( b "\/" a = Top L & b "/\" a = Bottom L ) by A1, LATTICES:def 18;
then ( b "\/" a = Top' L & b "/\" a = Bot' L ) by Th21, Th22;
then a is_a_complement'_of b by Def6;
hence ex a being Element of L st a is_a_complement'_of b ; :: thesis: verum

end;

hence L is complemented' by Def7; :: thesis: verum