:: deftheorem Def4 defines [# YELLOW11:def 4 :
for L being non empty RelStr
for a, b being Element of L
for b₄ being Subset of L holds
( b₄ = [#a,b#] iff for c being Element of L holds
( c in b₄ iff ( a <= c & c <= b ) ) );