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

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