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

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