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 object ; :: 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:39;
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