theorem Th40: :: OSAFREE:40

for S being monotone regular locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for t being Element of TS (DTConOSA X) holds
( (PTMin X) . t in OSClass ((PTCongruence X),t) & LeastSort ((PTMin X) . t) <= LeastSort t & ( for s being Element of S
for x being set st x in X . s & t = root-tree [x,s] holds
(PTMin X) . t = t ) & ( for o being OperSymbol of S
for ts being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots ts & t = (OSSym (o,X)) -tree ts holds
( LeastSorts ((PTMin X) * ts) <= the_arity_of o & OSSym (o,X) ==> roots ((PTMin X) * ts) & OSSym ((LBound (o,(LeastSorts ((PTMin X) * ts)))),X) ==> roots ((PTMin X) * ts) & (PTMin X) . t = (OSSym ((LBound (o,(LeastSorts ((PTMin X) * ts)))),X)) -tree ((PTMin X) * ts) ) ) )