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

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