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