let X be set ; :: thesis: for A, B, C being SetSequence of X st ( for n being Nat holds C . n = (A . n) \/ (B . n) ) holds
(lim_inf A) \/ (lim_inf B) c= lim_inf C
let A, B, C be SetSequence of X; :: thesis: ( ( for n being Nat holds C . n = (A . n) \/ (B . n) ) implies (lim_inf A) \/ (lim_inf B) c= lim_inf C )
assume A1: for n being Nat holds C . n = (A . n) \/ (B . n) ; :: thesis: (lim_inf A) \/ (lim_inf B) c= lim_inf C
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (lim_inf A) \/ (lim_inf B) or x in lim_inf C )
assume A2: x in (lim_inf A) \/ (lim_inf B) ; :: thesis: x in lim_inf C

per cases ( x in lim_inf A or x in lim_inf B ) by A2, XBOOLE_0:def 3;

suppose x in lim_inf A ; :: thesis: x in lim_inf C

then consider n being Nat such that
A3: for k being Nat holds x in A . (n + k) by Th4;
for k being Nat holds x in C . (n + k)

proof

let k be Nat; :: thesis: x in C . (n + k)
x in A . (n + k) by A3;
then x in (A . (n + k)) \/ (B . (n + k)) by XBOOLE_0:def 3;
hence x in C . (n + k) by A1; :: thesis: verum

end;

hence x in lim_inf C by Th4; :: thesis: verum

end;

suppose x in lim_inf B ; :: thesis: x in lim_inf C

then consider n being Nat such that
A4: for k being Nat holds x in B . (n + k) by Th4;
for k being Nat holds x in C . (n + k)

proof

let k be Nat; :: thesis: x in C . (n + k)
x in B . (n + k) by A4;
then x in (A . (n + k)) \/ (B . (n + k)) by XBOOLE_0:def 3;
hence x in C . (n + k) by A1; :: thesis: verum

end;

hence x in lim_inf C by Th4; :: thesis: verum

end;

end;