theorem :: SHEFFER1:22

for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr
for x, y being Element of L holds
( x is_a_complement'_of y iff x is_a_complement_of y ) by Th19, Th18;