let f be non empty FinSequence of NAT ; :: thesis: for X being disjoint_with_NAT set holds Terminals (DTConUA f,X) = X
let X be disjoint_with_NAT set ; :: thesis: Terminals (DTConUA f,X) = X
set A = DTConUA f,X;
A1: ( NonTerminals (DTConUA f,X) = dom f & Terminals (DTConUA f,X) misses NonTerminals (DTConUA f,X) & the carrier of (DTConUA f,X) = (Terminals (DTConUA f,X)) \/ (NonTerminals (DTConUA f,X)) ) by Th2, DTCONSTR:8, LANG1:1;
thus Terminals (DTConUA f,X) c= X by Th2; :: according to XBOOLE_0:def 10 :: thesis: X c= Terminals (DTConUA f,X)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Terminals (DTConUA f,X) )
assume A2: x in X ; :: thesis: x in Terminals (DTConUA f,X)
then A3: x in (dom f) \/ X by XBOOLE_0:def 3;

now

assume x in NonTerminals (DTConUA f,X) ; :: thesis: contradiction
then X meets NAT by A1, A2, XBOOLE_0:3;
hence contradiction by Def1; :: thesis: verum

end;

hence x in Terminals (DTConUA f,X) by A1, A3, XBOOLE_0:def 3; :: thesis: verum