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 & x in A |^ mn ) by Th19;
A3: x in (A |^ mn) \/ (B |^ mn) by A2, XBOOLE_0:def 3;
(A |^ mn) \/ (B |^ mn) c= (A \/ B) |^ mn by FLANG_1:39;
hence x in (A \/ B) |^ m,n by A2, A3, Th19; :: thesis: verum

end;

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

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

end;

end;