theorem Th20: :: OSALG_1:20

for S being OrderSortedSign
for w1, w2 being Element of the carrier of S *
for A being OSAlgebra of S st w1 <= w2 holds
( the Sorts of A #) . w1 c= ( the Sorts of A #) . w2