theorem Th63: :: AOFA_000:63

for X being non empty disjoint_with_NAT set
for C, I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds if-then-else (C,I1,I2) = 3 -tree <*C,I1,I2*>