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:31; :: thesis: verum