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)
thus for x being set st x in (A /\ B) |^.. k holds
x in (A |^.. k) /\ (B |^.. k) :: according to TARSKI:def 3 :: thesis: verum

proof

let x be set ; :: thesis: ( x in (A /\ B) |^.. k implies 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 & x in (A /\ B) |^ m ) by Th2;
(A /\ B) |^ m c= (A |^ m) /\ (B |^ m) by FLANG_1:40;
then A2: x in (A |^ m) /\ (B |^ m) by A1;
( A |^ m c= A |^.. k & B |^ m c= B |^.. k ) by A1, Th3;
then (A |^ m) /\ (B |^ m) c= (A |^.. k) /\ (B |^.. k) by XBOOLE_1:27;
hence x in (A |^.. k) /\ (B |^.. k) by A2; :: thesis: verum

end;