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) +

A1: A + = A |^.. 1 by Th50;

A2: B + = B |^.. 1 by Th50;

(A \/ B) + = (A \/ B) |^.. 1 by Th50;

hence (A +) \/ (B +) c= (A \/ B) + by A1, A2, Th45; :: thesis: verum

let A, B be Subset of (E ^omega); :: thesis: (A +) \/ (B +) c= (A \/ B) +

A1: A + = A |^.. 1 by Th50;

A2: B + = B |^.. 1 by Th50;

(A \/ B) + = (A \/ B) |^.. 1 by Th50;

hence (A +) \/ (B +) c= (A \/ B) + by A1, A2, Th45; :: thesis: verum