let E be set ; :: thesis: for A, B being Subset of (E ^omega ) holds (A + ) \/ (B + ) c= (A \/ B) +
let A, B be Subset of (E ^omega ); :: thesis: (A + ) \/ (B + ) c= (A \/ B) +
( (A \/ B) + = (A \/ B) |^.. 1 & A + = A |^.. 1 & B + = B |^.. 1 ) by Th50;
hence (A + ) \/ (B + ) c= (A \/ B) + by Th45; :: thesis: verum