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 CorNowosc1;
( AA = Inter (A ``1 ),(A ``2 ) & BB = Inter (B ``1 ),(B ``2 ) ) by Wazne33;
then ( min AA = A ``1 & min BB = B ``1 & max AA = A ``2 & max BB = B ``2 ) by nowosc2;
hence A _\_ B = Inter ((A ``1 ) \ (B ``2 )),((A ``2 ) \ (B ``1 )) by LemmaC0; :: thesis: verum