:: deftheorem Def12 defines LeastSort OSAFREE:def 12 :
for S being OrderSortedSign
for X being non-empty ManySortedSet of S
for t being Element of TS (DTConOSA X)
for b₄ being SortSymbol of S holds
( b₄ = LeastSort t iff ( t in the Sorts of (ParsedTermsOSA X) . b₄ & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
b₄ <= s1 ) ) );