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

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

suppose x in A |^.. k ; :: thesis: x in (A \/ B) |^.. k

then consider m being Nat such that
A2: k <= m and
A3: x in A |^ m by Th2;
A4: (A |^ m) \/ (B |^ m) c= (A \/ B) |^ m by FLANG_1:38;
A |^ m c= (A |^ m) \/ (B |^ m) by XBOOLE_1:7;
then A |^ m c= (A \/ B) |^ m by A4;
then A5: x in (A \/ B) |^ m by A3;
(A \/ B) |^ m c= (A \/ B) |^.. k by A2, Th3;
hence x in (A \/ B) |^.. k by A5; :: thesis: verum

end;

suppose x in B |^.. k ; :: thesis: x in (A \/ B) |^.. k

then consider m being Nat such that
A6: k <= m and
A7: x in B |^ m by Th2;
A8: (A |^ m) \/ (B |^ m) c= (A \/ B) |^ m by FLANG_1:38;
B |^ m c= (A |^ m) \/ (B |^ m) by XBOOLE_1:7;
then B |^ m c= (A \/ B) |^ m by A8;
then A9: x in (A \/ B) |^ m by A7;
(A \/ B) |^ m c= (A \/ B) |^.. k by A6, Th3;
hence x in (A \/ B) |^.. k by A9; :: thesis: verum

end;

end;