let A, B be SetSequence of the carrier of (TOP-REAL 2); :: thesis: for C being SetSequence of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) holds
Lim_sup C c= [:(Lim_sup A),(Lim_sup B):]
let C be SetSequence of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: ( ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) implies Lim_sup C c= [:(Lim_sup A),(Lim_sup B):] )
assume A1: for i being Element of NAT holds C . i = [:(A . i),(B . i):] ; :: thesis: Lim_sup C c= [:(Lim_sup A),(Lim_sup B):]
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Lim_sup C or x in [:(Lim_sup A),(Lim_sup B):] )
assume x in Lim_sup C ; :: thesis: x in [:(Lim_sup A),(Lim_sup B):]
then consider C1 being subsequence of C such that
A2: x in Lim_inf C1 by Def12;
consider A1, B1 being SetSequence of the carrier of (TOP-REAL 2) such that
A3: ( A1 is subsequence of A & B1 is subsequence of B & ( for i being Element of NAT holds C1 . i = [:(A1 . i),(B1 . i):] ) ) by A1, Th74;
x in the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] by A2;
then x in [:the carrier of (TOP-REAL 2),the carrier of (TOP-REAL 2):] by BORSUK_1:def 5;
then consider x1, x2 being set such that
A4: x = [x1,x2] by RELAT_1:def 1;
x in [:(Lim_inf A1),(Lim_inf B1):] by A2, A3, Th64;
then ( x1 in Lim_inf A1 & x2 in Lim_inf B1 ) by A4, ZFMISC_1:106;
then ( x1 in Lim_sup A & x2 in Lim_sup B ) by A3, Def12;
hence x in [:(Lim_sup A),(Lim_sup B):] by A4, ZFMISC_1:106; :: thesis: verum