theorem Th11: :: MSAFREE5:54

for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T deg<= 0 = { (x -term) where s is SortSymbol of S, x is Element of X . s : verum }