:: deftheorem defines is_a_complement'_of SHEFFER1:def 6 :
for L being non empty LattStr
for a, b being Element of L holds
( a is_a_complement'_of b iff ( b "\/" a = Top' L & a "\/" b = Top' L & b "/\" a = Bot' L & a "/\" b = Bot' L ) );