theorem :: WAYBEL_4:60

for L being complete LATTICE
for AR being Relation of L st ( for x being Element of L holds AR -below x is_directed_wrt AR ) holds
AR is satisfying_INT