reconsider CS = ContMaps S,T as full SubRelStr of T |^ the carrier of S by Def3;
CS is transitive ;
hence ContMaps S,T is transitive ; :: thesis: verum