let A, B be SetSequence of the carrier of (TOP-REAL 2); 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):]; ( ( 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):]
; Lim_sup C c= [:(Lim_sup A),(Lim_sup B):]
let x be object ; TARSKI:def 3 ( not x in Lim_sup C or x in [:(Lim_sup A),(Lim_sup B):] )
assume
x in Lim_sup C
; 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; verum