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

end;