theorem Th8: :: OSALG_3:8

for S1 being OrderSortedSign
for U1 being OSAlgebra of S1 holds U1,U1 are_os_isomorphic