let f be non empty FinSequence of NAT ; for X being disjoint_with_NAT set holds Terminals (DTConUA (f,X)) = X
let X be disjoint_with_NAT set ; Terminals (DTConUA (f,X)) = X
set A = DTConUA (f,X);
thus
Terminals (DTConUA (f,X)) c= X
by Th2; XBOOLE_0:def 10 X c= Terminals (DTConUA (f,X))
let x be object ; TARSKI:def 3 ( not x in X or x in Terminals (DTConUA (f,X)) )
assume A1:
x in X
; 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; verum