[:D1,D2:] c= [:the carrier of S1,the carrier of S2:] ;
hence [:D1,D2:] is Subset of [:S1,S2:] by Def2; :: thesis: verum