theorem Th60: :: AOFA_000:60

for X being non empty disjoint_with_NAT set
for p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) st 2 -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds
ex I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st p = <*I1,I2*>