theorem Th115: :: ABCMIZ_1:115

for D1, D2 being non empty DTConstrStr st the Rules of D1 c= the Rules of D2 holds
( NonTerminals D1 c= NonTerminals D2 & the carrier of D1 /\ (Terminals D2) c= Terminals D1 & ( Terminals D1 c= Terminals D2 implies the carrier of D1 c= the carrier of D2 ) )