:: deftheorem defines compact WAYBEL_3:def 2 :
for L being non empty reflexive RelStr
for x being Element of L holds
( x is compact iff x is_way_below x );