let E be set ; :: thesis: for A, B being Subset of (E ^omega )
for m, n being Nat holds (A /\ B) |^ m,n c= (A |^ m,n) /\ (B |^ m,n)
let A, B be Subset of (E ^omega ); :: thesis: for m, n being Nat holds (A /\ B) |^ m,n c= (A |^ m,n) /\ (B |^ m,n)
let m, n be Nat; :: thesis: (A /\ B) |^ m,n c= (A |^ m,n) /\ (B |^ m,n)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (A /\ B) |^ m,n or x in (A |^ m,n) /\ (B |^ m,n) )
assume x in (A /\ B) |^ m,n ; :: thesis: x in (A |^ m,n) /\ (B |^ m,n)
then consider mn being Nat such that
A1: ( m <= mn & mn <= n ) and
A2: x in (A /\ B) |^ mn by Th19;
A3: (A /\ B) |^ mn c= (A |^ mn) /\ (B |^ mn) by FLANG_1:40;
then x in B |^ mn by A2, XBOOLE_0:def 4;
then A4: x in B |^ m,n by A1, Th19;
x in A |^ mn by A2, A3, XBOOLE_0:def 4;
then x in A |^ m,n by A1, Th19;
hence x in (A |^ m,n) /\ (B |^ m,n) by A4, XBOOLE_0:def 4; :: thesis: verum