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 Wazne33, wazne2;
hence A is non empty ordered Subset-Family of U by nowosc1; :: thesis: verum