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 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 Nat holds C . i = [:(A . i),(B . i):] ) implies Lim_sup C c= [:(Lim_sup A),(Lim_sup B):] )
assume A1: for i being Nat holds C . i = [:(A . i),(B . i):] ; :: 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 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 Def2;
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 2;
then consider x1, x2 being object such that
A3: x = [x1,x2] by RELAT_1:def 1;
consider A1, B1 being SetSequence of the carrier of (TOP-REAL 2) such that
A4: A1 is subsequence of A and
A5: B1 is subsequence of B and
A6: for i being Nat holds C1 . i = [:(A1 . i),(B1 . i):] by A1, Th37;
A7: x in [:(Lim_inf A1),(Lim_inf B1):] by A2, A6, Th27;
then x2 in Lim_inf B1 by A3, ZFMISC_1:87;
then A8: x2 in Lim_sup B by A5, Def2;
x1 in Lim_inf A1 by A3, A7, ZFMISC_1:87;
then x1 in Lim_sup A by A4, Def2;
hence x in [:(Lim_sup A),(Lim_sup B):] by A3, A8, ZFMISC_1:87; :: thesis: verum