theorem Th36: :: OSAFREE:36

for S being locally_directed OrderSortedSign
for X being non-empty 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 )