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

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;

end;

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;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

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;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