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 ;

hereby :: thesis:

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

end;

let s9 be set ; :: thesis:
assume A4: ( s9 <> s or not x in X . s ) ; :: thesis:
set y = the Element of (X variables_in (root-tree [x,s])) . s9;
assume A5: (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 A5, FUNCT_1:def 2;
then A6: (X variables_in t) . s9 = (X . s9) /\ { (a `1) where a is Element of rng t : a `2 = s9 } by Th9;
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 A5, XBOOLE_0:def 4;
then consider a being Element of rng t such that
A7: ( 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 A4, A5, A6, A7, XBOOLE_0:def 4; :: thesis: