let X be set ; :: thesis: for A, B, C being SetSequence of X st ( for n being Nat holds C . n = (A . n) /\ (B . n) ) holds
lim_sup C c= (lim_sup A) /\ (lim_sup B)
let A, B, C be SetSequence of X; :: thesis: ( ( for n being Nat holds C . n = (A . n) /\ (B . n) ) implies lim_sup C c= (lim_sup A) /\ (lim_sup B) )
assume A1: for n being Nat holds C . n = (A . n) /\ (B . n) ; :: thesis: lim_sup C c= (lim_sup A) /\ (lim_sup B)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_sup C or x in (lim_sup A) /\ (lim_sup B) )
assume A2: x in lim_sup C ; :: thesis: x in (lim_sup A) /\ (lim_sup B)
for n being Nat ex k being Nat st x in B . (n + k)

proof

let n be Nat; :: thesis: ex k being Nat st x in B . (n + k)
consider k being Nat such that
A3: x in C . (n + k) by A2, Th5;
take k ; :: thesis: x in B . (n + k)
x in (A . (n + k)) /\ (B . (n + k)) by A1, A3;
hence x in B . (n + k) by XBOOLE_0:def 4; :: thesis: verum

end;

then A4: x in lim_sup B by Th5;
for n being Nat ex k being Nat st x in A . (n + k)

proof

let n be Nat; :: thesis: ex k being Nat st x in A . (n + k)
consider k being Nat such that
A5: x in C . (n + k) by A2, Th5;
take k ; :: thesis: x in A . (n + k)
x in (A . (n + k)) /\ (B . (n + k)) by A1, A5;
hence x in A . (n + k) by XBOOLE_0:def 4; :: thesis: verum

end;

then x in lim_sup A by Th5;
hence x in (lim_sup A) /\ (lim_sup B) by A4, XBOOLE_0:def 4; :: thesis: verum