let G be non empty DTConstrStr ; :: thesis: Terminals G misses NonTerminals G
A1: Terminals G = { t where t is Symbol of G : for tnt being FinSequence holds not t ==> tnt } by LANG1:def 2;
A2: NonTerminals G = { t where t is Symbol of G : ex tnt being FinSequence st t ==> tnt } by LANG1:def 3;
assume not Terminals G misses NonTerminals G ; :: thesis: contradiction
then consider x being object such that
A3: x in Terminals G and
A4: x in NonTerminals G by XBOOLE_0:3;
A5: ex t being Symbol of G st
( x = t & ( for tnt being FinSequence holds not t ==> tnt ) ) by A1, A3;
ex t being Symbol of G st
( x = t & ex tnt being FinSequence st t ==> tnt ) by A2, A4;
hence contradiction by A5; :: thesis: verum