:: deftheorem Def2 defines POSETS YELLOW21:def 2 :
for W, b₂ being set holds
( b₂ = POSETS W iff for x being object holds
( x in b₂ iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) );