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 object ; :: 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: not x in NonTerminals (DTConUA (f,X)) by A2, A1, Def1, XBOOLE_0:3;
( 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