let f be non empty FinSequence of NAT ; :: thesis: for D being non empty disjoint_with_NAT set holds not FreeGenSetNSG f,D is empty
let D be non empty disjoint_with_NAT set ; :: thesis: not FreeGenSetNSG f,D is empty
set X = DTConUA f,D;
consider d being Element of D;
reconsider d1 = d as Symbol of (DTConUA f,D) by XBOOLE_0:def 3;
Terminals (DTConUA f,D) = D by Th3;
then root-tree d1 in { (root-tree k) where k is Symbol of (DTConUA f,D) : k in Terminals (DTConUA f,D) } ;
hence not FreeGenSetNSG f,D is empty ; :: thesis: verum