:: deftheorem defines approximating WAYBEL_4:def 18 :
for L being non empty Poset
for mp being Function of L,(InclPoset (Ids L)) holds
( mp is approximating iff for x being Element of L ex ii being Subset of L st
( ii = mp . x & x = sup ii ) );