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 01: 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 00: 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 set ; :: 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
02: ( x = s & s ==> n ) ;
03: [s,n] in the Rules of D1 by 02, LANG1:def 1;
then [s,n] in the Rules of D2 by 01;
then reconsider s' = s as Symbol of D2 by ZFMISC_1:106;
s' ==> n by 01, 03, LANG1:def 1;
hence x in NonTerminals D2 by 02; :: 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 set ; :: thesis: ( x in the carrier of D1 /\ (Terminals D2) implies x in Terminals D1 )
assume x in the carrier of D1 /\ (Terminals D2) ; :: thesis: x in Terminals D1
then 04: ( x in the carrier of D1 & x in Terminals D2 & (Terminals D2) \/ (NonTerminals D2) = the carrier of D2 ) by LANG1:1, XBOOLE_0:def 4;
then reconsider s' = x as Symbol of D1 ;
reconsider s = x as Symbol of D2 by 04;
assume not x in Terminals D1 ; :: thesis: contradiction
then consider n being FinSequence such that
05: s' ==> n ;
[s',n] in the Rules of D1 by 05, LANG1:def 1;
then s ==> n by 01, LANG1:def 1;
then for s being Symbol of D2 holds
( not x = s or ex n being FinSequence st s ==> n ) ;
hence contradiction by 04; :: 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 00, 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