let x be set ; :: thesis: for S being non void Signature
for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( ( x in X . s & x in Y . s ) iff root-tree [x,s] in (() "" X) . s )

let S be non void Signature; :: thesis: for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( ( x in X . s & x in Y . s ) iff root-tree [x,s] in (() "" X) . s )

let Y be V8() ManySortedSet of the carrier of S; :: thesis: for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( ( x in X . s & x in Y . s ) iff root-tree [x,s] in (() "" X) . s )

let X be ManySortedSet of the carrier of S; :: thesis: for s being SortSymbol of S holds
( ( x in X . s & x in Y . s ) iff root-tree [x,s] in (() "" X) . s )

let s be SortSymbol of S; :: thesis: ( ( x in X . s & x in Y . s ) iff root-tree [x,s] in (() "" X) . s )
A1: (Reverse Y) . s = Reverse (s,Y) by MSAFREE:def 18;
A2: dom (Reverse (s,Y)) = FreeGen (s,Y) by FUNCT_2:def 1;
hereby :: thesis: ( root-tree [x,s] in (() "" X) . s implies ( x in X . s & x in Y . s ) )
assume that
A3: x in X . s and
A4: x in Y . s ; :: thesis: root-tree [x,s] in (() "" X) . s
A5: root-tree [x,s] in FreeGen (s,Y) by ;
[x,s] in the carrier of () by ;
then (() . s) . (root-tree [x,s]) = [x,s] `1 by
.= x ;
then root-tree [x,s] in (() . s) " (X . s) by ;
hence root-tree [x,s] in (() "" X) . s by EQUATION:def 1; :: thesis: verum
end;
assume root-tree [x,s] in (() "" X) . s ; :: thesis: ( x in X . s & x in Y . s )
then A6: root-tree [x,s] in (() . s) " (X . s) by EQUATION:def 1;
then A7: (Reverse (s,Y)) . (root-tree [x,s]) in X . s by ;
A8: root-tree [x,s] in FreeGen (s,Y) by ;
then consider z being set such that
A9: z in Y . s and
A10: root-tree [x,s] = root-tree [z,s] by MSAFREE:def 15;
B: [z,s] `1 = z ;
A11: [x,s] = [z,s] by ;
then [x,s] in the carrier of () by ;
then [x,s] `1 in X . s by ;
hence ( x in X . s & x in Y . s ) by A9, A11, B; :: thesis: verum