let X be set ; :: thesis: for A1, A2 being SetSequence of X holds lim_sup (A1 (\/) A2) = (lim_sup A1) \/ (lim_sup A2)
let A1, A2 be SetSequence of X; :: thesis: lim_sup (A1 (\/) A2) = (lim_sup A1) \/ (lim_sup A2)
for n being Nat holds (A1 (\/) A2) . n = (A1 . n) \/ (A2 . n) by Def2;
hence lim_sup (A1 (\/) A2) = (lim_sup A1) \/ (lim_sup A2) by KURATO_0:11; :: thesis: verum