let X be set ; :: thesis: for A1, A2 being SetSequence of X holds lim_sup (A1 (/\) A2) c= (lim_sup A1) /\ (lim_sup A2)
let A1, A2 be SetSequence of X; :: thesis: lim_sup (A1 (/\) A2) c= (lim_sup A1) /\ (lim_sup A2)
for n being Element of NAT holds (A1 (/\) A2) . n = (A1 . n) /\ (A2 . n) by Def1;
hence lim_sup (A1 (/\) A2) c= (lim_sup A1) /\ (lim_sup A2) by KURATO_0:13; :: thesis: verum