:: deftheorem defines interval YELLOW11:def 5 :
for L being non empty RelStr
for IT being Subset of L holds
( IT is interval iff ex a, b being Element of L st IT = [#a,b#] );