theorem Th20: :: OSALG_4:20

for S being OrderSortedSign
for U1 being non-empty OSAlgebra of S holds [| the Sorts of U1, the Sorts of U1|] is OSCongruence of U1