let x be set ; :: thesis: for S being non void Signature
for Y being non-empty 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 ((Reverse Y) "" X) . s )
let S be non void Signature; :: thesis: for Y being non-empty 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 ((Reverse Y) "" X) . s )
let Y be non-empty 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 ((Reverse Y) "" 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 ((Reverse Y) "" X) . s )
let s be SortSymbol of S; :: thesis: ( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" 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 ((Reverse Y) "" 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 ((Reverse Y) "" X) . s
A5: root-tree [x,s] in FreeGen (s,Y) by A4, MSAFREE:def 15;
[x,s] in the carrier of (DTConMSA Y) by A4, Th2;
then ((Reverse Y) . s) . (root-tree [x,s]) = [x,s] `1 by A1, A5, MSAFREE:def 17
.= x ;
then root-tree [x,s] in ((Reverse Y) . s) " (X . s) by A1, A2, A3, A5, FUNCT_1:def 7;
hence root-tree [x,s] in ((Reverse Y) "" X) . s by EQUATION:def 1; :: thesis: verum

end;

assume root-tree [x,s] in ((Reverse Y) "" X) . s ; :: thesis: ( x in X . s & x in Y . s )
then A6: root-tree [x,s] in ((Reverse Y) . s) " (X . s) by EQUATION:def 1;
then A7: (Reverse (s,Y)) . (root-tree [x,s]) in X . s by A1, FUNCT_1:def 7;
A8: root-tree [x,s] in FreeGen (s,Y) by A1, A2, A6, FUNCT_1:def 7;
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 A10, TREES_4:4;
then [x,s] in the carrier of (DTConMSA Y) by A9, Th2;
then [x,s] `1 in X . s by A8, A7, MSAFREE:def 17;
hence ( x in X . s & x in Y . s ) by A9, A11, B; :: thesis: verum