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