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