let U be non empty set ; :: thesis: for A, B being non empty IntervalSet of U holds A _/\_ (A _\/_ B) = A
let A, B be non empty IntervalSet of U; :: thesis: A _/\_ (A _\/_ B) = A
( A is non empty ordered Subset-Family of U & B is non empty ordered Subset-Family of U ) by Lm4;
hence A _/\_ (A _\/_ B) = A by Th33; :: thesis: verum