:: deftheorem Def13 defines MonSet WAYBEL_4:def 13 :
for L being non empty Poset
for b₂ being strict RelStr holds
( b₂ = MonSet L iff for a being set holds
( ( a in the carrier of b₂ implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of b₂ ) & ( for c, d being object holds
( [c,d] in the InternalRel of b₂ iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of b₂ & d in the carrier of b₂ & f <= g ) ) ) ) );