let X be non empty disjoint_with_NAT set ; :: thesis: for I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds
( I1 \; I2 <> I1 & I1 \; I2 <> I2 )
set S = ECIW-signature ;
set G = DTConUA (ECIW-signature,X);
set A = FreeUnivAlgNSG (ECIW-signature,X);
let I1, I2 be Element of (FreeUnivAlgNSG (ECIW-signature,X)); :: thesis: ( I1 \; I2 <> I1 & I1 \; I2 <> I2 )
set p = <*I1,I2*>;
rng <*I1,I2*> c= FinTrees the carrier of (DTConUA (ECIW-signature,X)) by XBOOLE_1:1;
then A1: <*I1,I2*> is FinSequence of FinTrees the carrier of (DTConUA (ECIW-signature,X)) by FINSEQ_1:def 4;
A2: rng <*I1,I2*> = {I1,I2} by FINSEQ_2:127;
then A3: I1 in rng <*I1,I2*> by TARSKI:def 2;
A4: I2 in rng <*I1,I2*> by A2, TARSKI:def 2;
I1 \; I2 = 2 -tree (I1,I2) by Th59
.= 2 -tree <*I1,I2*> ;
hence ( I1 \; I2 <> I1 & I1 \; I2 <> I2 ) by A1, A3, A4, Th3; :: thesis: verum