theorem Th58: :: AOFA_000:58

for X being non empty disjoint_with_NAT set
for p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) st 1 -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds
p = {}