:: deftheorem Def2 defines interval LFUZZY_0:def 2 :
for R being RelStr holds
( R is interval iff ( R is real & ex a, b being Real st
( a <= b & the carrier of R = [.a,b.] ) ) );