theorem Th29: :: OSALG_2:29

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds
( OSMSubSort A is opers_closed & A c= OSMSubSort A )