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 set such that
A3: ( x in Terminals G & x in NonTerminals G ) by XBOOLE_0:3;
( ex t being Symbol of G st
( x = t & ( for tnt being FinSequence holds not t ==> tnt ) ) & ex t being Symbol of G st
( x = t & ex tnt being FinSequence st t ==> tnt ) ) by A1, A2, A3;
hence contradiction ; :: thesis: verum