:: deftheorem Def3 defines satisfying_axiom_K WAYBEL_8:def 3 :
for L being non empty reflexive RelStr holds
( L is satisfying_axiom_K iff for x being Element of L holds x = sup (compactbelow x) );