:: deftheorem defines OSbool OSALG_2:def 6 :
for R being non empty Poset
for M being OrderSortedSet of R
for b₃ being set holds
( b₃ = OSbool M iff for x being set holds
( x in b₃ iff x is OrderSortedSubset of M ) );