let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X holds A \+\ (lim_sup A1) c= lim_sup (A (\+\) A1)
let A be Subset of X; :: thesis: for A1 being SetSequence of X holds A \+\ (lim_sup A1) c= lim_sup (A (\+\) A1)
let A1 be SetSequence of X; :: thesis: A \+\ (lim_sup A1) c= lim_sup (A (\+\) A1)
for n being Nat holds (A (\+\) A1) . n = A \+\ (A1 . n) by Def9;
hence A \+\ (lim_sup A1) c= lim_sup (A (\+\) A1) by KURATO_0:17; :: thesis: verum