theorem Th19: :: OSALG_2:19

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A, B being OSSubset of OU0 holds
( B in OSSubSort A iff ( B is opers_closed & OSConstants OU0 c= B & A c= B ) )