let X be set ; :: thesis: for A1, A2 being SetSequence of X st ( A1 is convergent or A2 is convergent ) holds
lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2)
let A1, A2 be SetSequence of X; :: thesis: ( ( A1 is convergent or A2 is convergent ) implies lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2) )
A1: for A1, A2 being SetSequence of X st A1 is convergent holds
lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2)

proof

let A1, A2 be SetSequence of X; :: thesis: ( A1 is convergent implies lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2) )
assume A2: A1 is convergent ; :: thesis: lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2)
thus lim_inf (A1 (\/) A2) c= (lim_inf A1) \/ (lim_inf A2) :: according to XBOOLE_0:def 10 :: thesis: (lim_inf A1) \/ (lim_inf A2) c= lim_inf (A1 (\/) A2)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_inf (A1 (\/) A2) or x in (lim_inf A1) \/ (lim_inf A2) )
assume x in lim_inf (A1 (\/) A2) ; :: thesis: x in (lim_inf A1) \/ (lim_inf A2)
then consider n1 being Nat such that
A3: for k being Nat holds x in (A1 (\/) A2) . (n1 + k) by KURATO_0:4;

A4: now :: thesis: for n being Nat holds
( x in A1 . (n1 + n) or x in A2 . (n1 + n) )

let n be Nat; :: thesis: ( x in A1 . (n1 + n) or x in A2 . (n1 + n) )
x in (A1 (\/) A2) . (n1 + n) by A3;
then x in (A1 . (n1 + n)) \/ (A2 . (n1 + n)) by Def2;
hence ( x in A1 . (n1 + n) or x in A2 . (n1 + n) ) by XBOOLE_0:def 3; :: thesis: verum

end;

x in (lim_inf A1) \/ (lim_inf A2)

proof

assume A5: not x in (lim_inf A1) \/ (lim_inf A2) ; :: thesis: contradiction
then not x in lim_inf A1 by XBOOLE_0:def 3;
then not x in lim_sup A1 by A2, KURATO_0:def 5;
then consider n2 being Nat such that
A6: for k being Nat holds not x in A1 . (n2 + k) by KURATO_0:5;
not x in lim_inf A2 by A5, XBOOLE_0:def 3;
then consider k1 being Nat such that
A7: not x in A2 . ((n1 + n2) + k1) by KURATO_0:4;
not x in A1 . (n2 + (n1 + k1)) by A6;
then not x in A1 . (n1 + (n2 + k1)) ;
hence contradiction by A4, A7; :: thesis: verum

end;

hence x in (lim_inf A1) \/ (lim_inf A2) ; :: thesis: verum

end;

thus (lim_inf A1) \/ (lim_inf A2) c= lim_inf (A1 (\/) A2) by Th61; :: thesis: verum

end;

assume A8: ( A1 is convergent or A2 is convergent ) ; :: thesis: lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2)

per cases ( A1 is convergent or A2 is convergent ) by A8;

suppose A1 is convergent ; :: thesis: lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2)

hence lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2) by A1; :: thesis: verum

end;

suppose A2 is convergent ; :: thesis: lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2)

hence lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2) by A1; :: thesis: verum

end;

end;