ContMaps (S,T) is non empty full sups-inheriting SubRelStr of T |^ the carrier of S by Def3, Th35;
hence ContMaps (S,T) is complete by YELLOW_2:33; :: thesis: verum