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 )