for L being non empty complete Poset holds
( (IdsMap L) * (SupMap L) is closure & Image ((IdsMap L) * (SupMap L)),L are_isomorphic )