ContMaps X,L is full directed-sups-inheriting SubRelStr of L |^ the carrier of X by Th12, WAYBEL24:def 3;
hence ContMaps X,L is up-complete by YELLOW16:5; :: thesis: verum