theorem Th48: :: WAYBEL_4:48

for L being complete LATTICE
for x, y being Element of L
for AR being approximating Relation of L st not x <= y holds
ex u being Element of L st
( [u,x] in AR & not u <= y )