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;
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 A1: x in X ; :: thesis: x in Terminals (DTConUA f,X)
A2: NonTerminals (DTConUA f,X) = dom f by Th2;

A3: now

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

end;

( the carrier of (DTConUA f,X) = (Terminals (DTConUA f,X)) \/ (NonTerminals (DTConUA f,X)) & x in (dom f) \/ X ) by A1, LANG1:1, XBOOLE_0:def 3;
hence x in Terminals (DTConUA f,X) by A3, XBOOLE_0:def 3; :: thesis: verum