for S being locally_directed OrderSortedSign
for X being V2() ManySortedSet of S
for s being Element of S
for t being Element of TS (DTConOSA X)
for x, x1 being set st x in X . s & t = root-tree [x,s] holds
( x1 in OSClass ((LCongruence X),t) iff x1 = t )