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);
set d = the Element of D;
reconsider d1 = the Element of 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