let X be non empty disjoint_with_NAT set ; 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); ( 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:147;
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; verum