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

for b being Element of L ex a being Element of L st a is_a_complement'_of b

proof

hence
L is complemented'
; :: thesis: verum
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;

take a ; :: thesis: a is_a_complement'_of b

A2: b "/\" a = Bottom L by A1;

b "\/" a = Top L by A1;

hence ( b "\/" a = Top' L & a "\/" b = Top' L & b "/\" a = Bot' L & a "/\" b = Bot' L ) by A2, Th20, Th21; :: according to SHEFFER1:def 6 :: thesis: verum

end;consider a being Element of L such that

A1: a is_a_complement_of b by LATTICES:def 19;

take a ; :: thesis: a is_a_complement'_of b

A2: b "/\" a = Bottom L by A1;

b "\/" a = Top L by A1;

hence ( b "\/" a = Top' L & a "\/" b = Top' L & b "/\" a = Bot' L & a "/\" b = Bot' L ) by A2, Th20, Th21; :: according to SHEFFER1:def 6 :: thesis: verum