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