let D1, D2 be non empty DTConstrStr ; :: thesis: ( the Rules of D1 c= the Rules of D2 implies ( 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 ) ) )
assume A1: the Rules of D1 c= the Rules of D2 ; :: thesis: ( 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 ) )
thus A2: NonTerminals D1 c= NonTerminals D2 :: thesis: ( the carrier of D1 /\ (Terminals D2) c= Terminals D1 & ( Terminals D1 c= Terminals D2 implies the carrier of D1 c= the carrier of D2 ) )

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NonTerminals D1 or x in NonTerminals D2 )
assume x in NonTerminals D1 ; :: thesis: x in NonTerminals D2
then ex s being Symbol of D1 st
( x = s & ex n being FinSequence st s ==> n ) ;
then consider s being Symbol of D1, n being FinSequence such that
A3: x = s and
A4: s ==> n ;
A5: [s,n] in the Rules of D1 by A4;
then [s,n] in the Rules of D2 by A1;
then reconsider s9 = s as Symbol of D2 by ZFMISC_1:87;
s9 ==> n by A1, A5;
hence x in NonTerminals D2 by A3; :: thesis: verum

end;

hereby :: according to TARSKI:def 3 :: thesis: ( Terminals D1 c= Terminals D2 implies the carrier of D1 c= the carrier of D2 )

let x be object ; :: thesis: ( x in the carrier of D1 /\ (Terminals D2) implies x in Terminals D1 )
assume A6: x in the carrier of D1 /\ (Terminals D2) ; :: thesis: x in Terminals D1
then A7: x in Terminals D2 by XBOOLE_0:def 4;
reconsider s9 = x as Symbol of D1 by A6, XBOOLE_0:def 4;
reconsider s = x as Symbol of D2 by A6;
assume not x in Terminals D1 ; :: thesis: contradiction
then consider n being FinSequence such that
A8: s9 ==> n ;
[s9,n] in the Rules of D1 by A8;
then s ==> n by A1;
then for s being Symbol of D2 holds
( not x = s or ex n being FinSequence st s ==> n ) ;
hence contradiction by A7; :: thesis: verum

end;

assume Terminals D1 c= Terminals D2 ; :: thesis: the carrier of D1 c= the carrier of D2
then (Terminals D1) \/ (NonTerminals D1) c= (Terminals D2) \/ (NonTerminals D2) by A2, XBOOLE_1:13;
then (Terminals D1) \/ (NonTerminals D1) c= the carrier of D2 by LANG1:1;
hence the carrier of D1 c= the carrier of D2 by LANG1:1; :: thesis: verum