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