let U be non empty set ; :: thesis: for A being non empty IntervalSet of U holds A is non empty ordered Subset-Family of U
let A be non empty IntervalSet of U; :: thesis: A is non empty ordered Subset-Family of U
( A = Inter ((A ``1),(A ``2)) & A ``1 c= A ``2 ) by Th15, Th16;
hence A is non empty ordered Subset-Family of U by Th25; :: thesis: verum