:: deftheorem Def8 defines ordered INTERVA1:def 8 :
for X being set
for F being Subset-Family of X holds
( F is ordered iff ex A, B being set st
( A in F & B in F & ( for Y being set holds
( Y in F iff ( A c= Y & Y c= B ) ) ) ) );