theorem Th49: :: WAYBEL_4:49

for L being complete LATTICE
for x, z being Element of L
for R being auxiliary(i) auxiliary(iii) approximating Relation of L st [x,z] in R & x <> z holds
ex y being Element of L st
( x <= y & [y,z] in R & x <> y )