for R being upper-bounded Semilattice
for X being Subset of [:R,R:] st ex_inf_of (inf_op R) .: X,R holds
inf_op R preserves_inf_of X