:: deftheorem defines is_a_complement_of LATTICES:def 18 :
for L being non empty LattStr
for a, b being Element of L holds
( a is_a_complement_of b iff ( a "\/" b = Top L & b "\/" a = Top L & a "/\" b = Bottom L & b "/\" a = Bottom L ) );