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 object ; :: 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:38;
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:38;
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;