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