let U be non empty set ; :: thesis: for A being non empty IntervalSet of U holds A is non empty ordered Subset-Family of
let A be non empty IntervalSet of U; :: thesis: A is non empty ordered Subset-Family of
consider A1, A2 being Subset of such that
a0: ( A1 c= A2 & A = Inter A1,A2 ) by U2;
( A1 in A & A2 in A & ( for Y being set holds
( Y in A iff ( A1 c= Y & Y c= A2 ) ) ) ) by a0, Lemacik;
hence A is non empty ordered Subset-Family of by DefOr; :: thesis: verum