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