theorem :: WAYBEL_4:59

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