let x be set ; :: thesis: for S being non void Signature
for Y being V5() ManySortedSet of
for X being ManySortedSet of
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 V5() ManySortedSet of
for X being ManySortedSet of
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 V5() ManySortedSet of ; :: thesis: for X being ManySortedSet of
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 ; :: 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 & dom (Reverse s,Y) = FreeGen s,Y ) by FUNCT_2:def 1, MSAFREE:def 20;

hereby :: thesis: ( root-tree [x,s] in ((Reverse Y) "" X) . s implies ( x in X . s & x in Y . s ) )

assume A2: ( x in X . s & x in Y . s ) ; :: thesis: root-tree [x,s] in ((Reverse Y) "" X) . s
then A3: ( root-tree [x,s] in FreeGen s,Y & [x,s] in the carrier of (DTConMSA Y) ) by Th3, MSAFREE:def 17;
then ((Reverse Y) . s) . (root-tree [x,s]) = [x,s] `1 by A1, MSAFREE:def 19
.= x by MCART_1:7 ;
then root-tree [x,s] in ((Reverse Y) . s) " (X . s) by A1, A2, A3, FUNCT_1:def 13;
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 root-tree [x,s] in ((Reverse Y) . s) " (X . s) by EQUATION:def 1;
then A4: ( root-tree [x,s] in FreeGen s,Y & (Reverse s,Y) . (root-tree [x,s]) in X . s ) by A1, FUNCT_1:def 13;
then consider z being set such that
A5: ( z in Y . s & root-tree [x,s] = root-tree [z,s] ) by MSAFREE:def 17;
A6: [x,s] = [z,s] by A5, TREES_4:4;
then [x,s] in the carrier of (DTConMSA Y) by A5, Th3;
then [x,s] `1 in X . s by A4, MSAFREE:def 19;
hence ( x in X . s & x in Y . s ) by A5, A6, MCART_1:7, ZFMISC_1:33; :: thesis: verum