let S be ManySortedSign ; :: thesis:
let X be ManySortedSet of ; :: thesis:
let s, x be set ; :: thesis:
reconsider t = root-tree [x,s] as DecoratedTree ;
t = {[{} ,[x,s]]} by TREES_4:6;
then A1: rng t = {[x,s]} by RELAT_1:23;
A2: ( [x,s] `1 = x & [x,s] `2 = s ) by MCART_1:7;

hereby :: thesis:

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

end;

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