let E be set ; :: thesis: for A, B being Subset of ()
for k being Nat holds (A |^.. k) \/ (B |^.. k) c= (A \/ B) |^.. k

let A, B be Subset of (); :: 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 ;
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 ;
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 ;
hence x in (A \/ B) |^.. k by A9; :: thesis: verum
end;
end;