:: deftheorem defines @ OSALG_2:def 9 :
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for e being Element of OSSubSort OU0 holds @ e = e;