let U be non empty set ; :: thesis: for A, B being non empty IntervalSet of U holds A _\_ B = Inter (((A ``1) \ (B ``2)),((A ``2) \ (B ``1)))
let A, B be non empty IntervalSet of U; :: thesis: A _\_ B = Inter (((A ``1) \ (B ``2)),((A ``2) \ (B ``1)))
reconsider AA = A, BB = B as non empty ordered Subset-Family of U by Th26;
( AA = Inter ((A ``1),(A ``2)) & BB = Inter ((B ``1),(B ``2)) ) by Th15;
then ( min AA = A ``1 & min BB = B ``1 & max AA = A ``2 & max BB = B ``2 ) by Th27;
hence A _\_ B = Inter (((A ``1) \ (B ``2)),((A ``2) \ (B ``1))) by Th38; :: thesis: verum