theorem Th61: :: AOFA_000:61
for X being non empty disjoint_with_NAT set
for I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds
( I1 \; I2 <> I1 & I1 \; I2 <> I2 )