let S be ManySortedSign ; :: thesis:
let X be ManySortedSet of the carrier of S; :: thesis:
let s, x be set ; :: thesis:
reconsider t = root-tree [x,s] as DecoratedTree ;
A1: ( [x,s] `1 = x & [x,s] `2 = s ) by MCART_1:7;

hereby :: thesis:

assume A2: x in X . s ; :: thesis:
then A3: {x} c= X . s by ZFMISC_1:31;
dom X = the carrier of S by PARTFUN1:def 2;
then A4: s in the carrier of S by A2, FUNCT_1:def 2;
then (S variables_in (root-tree [x,s])) . s = {x} by Th11;
then (X . s) /\ ((S variables_in (root-tree [x,s])) . s) = {x} by A3, XBOOLE_1:28;
hence (X variables_in (root-tree [x,s])) . s = {x} by A4, PBOOLE:def 5; :: thesis:

end;

let s9 be set ; :: thesis:
assume A5: ( s9 <> s or not x in X . s ) ; :: thesis:
set y = the Element of (X variables_in (root-tree [x,s])) . s9;
assume A6: (X variables_in (root-tree [x,s])) . s9 <> {} ; :: thesis:
dom (X variables_in t) = the carrier of S by PARTFUN1:def 2;
then s9 in the carrier of S by A6, FUNCT_1:def 2;
then A7: (X variables_in t) . s9 = (X . s9) /\ { (a `1) where a is Element of rng t : a `2 = s9 } by Th10;
then the Element of (X variables_in (root-tree [x,s])) . s9 in { (a `1) where a is Element of rng t : a `2 = s9 } by A6, XBOOLE_0:def 4;
then consider a being Element of rng t such that
A8: ( the Element of (X variables_in (root-tree [x,s])) . s9 = a `1 & a `2 = s9 ) ;
t = {[{},[x,s]]} by TREES_4:6;
then rng t = {[x,s]} by RELAT_1:9;
then a = [x,s] by TARSKI:def 1;
hence contradiction by A1, A5, A6, A7, A8, XBOOLE_0:def 4; :: thesis: