:: deftheorem defines preserves_inf_of WAYBEL_0:def 30 :
for S, T being non empty RelStr
for f being Function of S,T
for X being Subset of S holds
( f preserves_inf_of X iff ( ex_inf_of X,S implies ( ex_inf_of f .: X,T & inf (f .: X) = f . (inf X) ) ) );