:: deftheorem defines complemented WAYBEL_1:def 24 :
for L being non empty RelStr holds
( L is complemented iff for x being Element of L ex y being Element of L st y is_a_complement_of x );