for L being non empty Poset holds
( dom (SupMap L) = Ids L & rng (SupMap L) is Subset of L )