let E be set ; :: thesis: for A, B being Subset of (E ^omega)

for k being Nat holds (A /\ B) |^.. k c= (A |^.. k) /\ (B |^.. k)

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

let k be Nat; :: thesis: (A /\ B) |^.. k c= (A |^.. k) /\ (B |^.. k)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A /\ B) |^.. k or x in (A |^.. k) /\ (B |^.. k) )

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

then consider m being Nat such that

A1: k <= m and

A2: x in (A /\ B) |^ m by Th2;

A3: B |^ m c= B |^.. k by A1, Th3;

(A /\ B) |^ m c= (A |^ m) /\ (B |^ m) by FLANG_1:39;

then A4: x in (A |^ m) /\ (B |^ m) by A2;

A |^ m c= A |^.. k by A1, Th3;

then (A |^ m) /\ (B |^ m) c= (A |^.. k) /\ (B |^.. k) by A3, XBOOLE_1:27;

hence x in (A |^.. k) /\ (B |^.. k) by A4; :: thesis: verum

for k being Nat holds (A /\ B) |^.. k c= (A |^.. k) /\ (B |^.. k)

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

let k be Nat; :: thesis: (A /\ B) |^.. k c= (A |^.. k) /\ (B |^.. k)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A /\ B) |^.. k or x in (A |^.. k) /\ (B |^.. k) )

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

then consider m being Nat such that

A1: k <= m and

A2: x in (A /\ B) |^ m by Th2;

A3: B |^ m c= B |^.. k by A1, Th3;

(A /\ B) |^ m c= (A |^ m) /\ (B |^ m) by FLANG_1:39;

then A4: x in (A |^ m) /\ (B |^ m) by A2;

A |^ m c= A |^.. k by A1, Th3;

then (A |^ m) /\ (B |^ m) c= (A |^.. k) /\ (B |^.. k) by A3, XBOOLE_1:27;

hence x in (A |^.. k) /\ (B |^.. k) by A4; :: thesis: verum