let E be set ; :: thesis: for A, B being Subset of (E ^omega )
for m, n being Nat holds (A |^ m,n) \/ (B |^ m,n) c= (A \/ B) |^ m,n
let A, B be Subset of (E ^omega ); :: thesis: for m, n being Nat holds (A |^ m,n) \/ (B |^ m,n) c= (A \/ B) |^ m,n
let m, n be Nat; :: thesis: (A |^ m,n) \/ (B |^ m,n) c= (A \/ B) |^ m,n
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (A |^ m,n) \/ (B |^ m,n) or x in (A \/ B) |^ m,n )
assume A1: x in (A |^ m,n) \/ (B |^ m,n) ; :: thesis: x in (A \/ B) |^ m,n

per cases ( x in A |^ m,n or x in B |^ m,n ) by A1, XBOOLE_0:def 3;

suppose x in A |^ m,n ; :: thesis: x in (A \/ B) |^ m,n

then consider mn being Nat such that
A2: ( m <= mn & mn <= n ) and
A3: x in A |^ mn by Th19;
A4: (A |^ mn) \/ (B |^ mn) c= (A \/ B) |^ mn by FLANG_1:39;
x in (A |^ mn) \/ (B |^ mn) by A3, XBOOLE_0:def 3;
hence x in (A \/ B) |^ m,n by A2, A4, Th19; :: thesis: verum

end;

suppose x in B |^ m,n ; :: thesis: x in (A \/ B) |^ m,n

then consider mn being Nat such that
A5: ( m <= mn & mn <= n ) and
A6: x in B |^ mn by Th19;
A7: (A |^ mn) \/ (B |^ mn) c= (A \/ B) |^ mn by FLANG_1:39;
x in (A |^ mn) \/ (B |^ mn) by A6, XBOOLE_0:def 3;
hence x in (A \/ B) |^ m,n by A5, A7, Th19; :: thesis: verum

end;

end;