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 * c= (A \/ B) * & B * c= (A \/ B) * ) by Th61, XBOOLE_1:7;
hence (A *) \/ (B *) c= (A \/ B) * by XBOOLE_1:8; :: thesis: verum