let X be set ; :: thesis: for A1, A2 being SetSequence of X st ( A1 is convergent or A2 is convergent ) holds
lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2)
let A1, A2 be SetSequence of X; :: thesis: ( ( A1 is convergent or A2 is convergent ) implies lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2) )
A1: for A1, A2 being SetSequence of X st A1 is convergent holds
lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2)

proof

let A1, A2 be SetSequence of X; :: thesis: ( A1 is convergent implies lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2) )
assume A2: A1 is convergent ; :: thesis: lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2)
thus lim_sup (A1 (/\) A2) c= (lim_sup A1) /\ (lim_sup A2) by Th67; :: according to XBOOLE_0:def 10 :: thesis: (lim_sup A1) /\ (lim_sup A2) c= lim_sup (A1 (/\) A2)
thus (lim_sup A1) /\ (lim_sup A2) c= lim_sup (A1 (/\) A2) :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (lim_sup A1) /\ (lim_sup A2) or x in lim_sup (A1 (/\) A2) )
assume A3: x in (lim_sup A1) /\ (lim_sup A2) ; :: thesis: x in lim_sup (A1 (/\) A2)
then x in lim_sup A1 by XBOOLE_0:def 4;
then x in lim_inf A1 by A2, KURATO_0:def 5;
then consider n1 being Nat such that
A4: for k being Nat holds x in A1 . (n1 + k) by KURATO_0:4;
A5: x in lim_sup A2 by A3, XBOOLE_0:def 4;

now :: thesis: for n being Nat ex k being Nat st x in (A1 (/\) A2) . (n + k)

let n be Nat; :: thesis: ex k being Nat st x in (A1 (/\) A2) . (n + k)
consider k1 being Nat such that
A6: x in A2 . ((n + n1) + k1) by A5, KURATO_0:5;
x in A1 . (n1 + (n + k1)) by A4;
then x in (A1 . (n + (n1 + k1))) /\ (A2 . (n + (n1 + k1))) by A6, XBOOLE_0:def 4;
then x in (A1 (/\) A2) . (n + (n1 + k1)) by Def1;
hence ex k being Nat st x in (A1 (/\) A2) . (n + k) ; :: thesis: verum

end;

hence x in lim_sup (A1 (/\) A2) by KURATO_0:5; :: thesis: verum

end;

end;

assume A7: ( A1 is convergent or A2 is convergent ) ; :: thesis: lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2)

per cases ( A1 is convergent or A2 is convergent ) by A7;

suppose A1 is convergent ; :: thesis: lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2)

hence lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2) by A1; :: thesis: verum

end;

suppose A2 is convergent ; :: thesis: lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2)

hence lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2) by A1; :: thesis: verum

end;

end;