let X be set ; :: thesis: for A1, A2 being SetSequence of X st A1 is convergent & 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 & A2 is convergent implies lim_sup (A1 (\+\) A2) = (lim_sup A1) \+\ (lim_sup A2) )
assume that
A1: A1 is convergent and
A2: A2 is convergent ; :: thesis: lim_sup (A1 (\+\) A2) = (lim_sup A1) \+\ (lim_sup A2)
thus lim_sup (A1 (\+\) A2) = lim_sup ((A1 (\) A2) (\/) (A2 (\) A1)) by Th3
.= (lim_sup (A1 (\) A2)) \/ (lim_sup (A2 (\) A1)) by Th68
.= ((lim_sup A1) \ (lim_sup A2)) \/ (lim_sup (A2 (\) A1)) by A2, Th72
.= (lim_sup A1) \+\ (lim_sup A2) by A1, Th72 ; :: thesis: verum