for L being complete LATTICE
for mp being Function of L,(InclPoset (Ids L)) st mp is approximating & mp in the carrier of (MonSet L) holds
ex AR being auxiliary approximating Relation of L st AR = (Map2Rel L) . mp