let X be set ; :: thesis: for A, B, C being SetSequence of X st ( for n being Element of NAT holds C . n = (A . n) /\ (B . n) ) holds
lim_inf C = (lim_inf A) /\ (lim_inf B)
let A, B, C be SetSequence of X; :: thesis: ( ( for n being Element of NAT holds C . n = (A . n) /\ (B . n) ) implies lim_inf C = (lim_inf A) /\ (lim_inf B) )
assume A1: for n being Element of NAT holds C . n = (A . n) /\ (B . n) ; :: thesis: lim_inf C = (lim_inf A) /\ (lim_inf B)
thus lim_inf C c= (lim_inf A) /\ (lim_inf B) :: according to XBOOLE_0:def 10 :: thesis: (lim_inf A) /\ (lim_inf B) c= lim_inf C

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_inf C or x in (lim_inf A) /\ (lim_inf B) )
assume x in lim_inf C ; :: thesis: x in (lim_inf A) /\ (lim_inf B)
then consider n being Element of NAT such that
A2: for k being Element of NAT holds x in C . (n + k) by Th7;
for k being Element of NAT holds x in A . (n + k)

proof

let k be Element of NAT ; :: thesis: x in A . (n + k)
A3: C . (n + k) = (A . (n + k)) /\ (B . (n + k)) by A1;
x in C . (n + k) by A2;
hence x in A . (n + k) by A3, XBOOLE_0:def 4; :: thesis: verum

end;

then A4: x in lim_inf A by Th7;
for k being Element of NAT holds x in B . (n + k)

proof

let k be Element of NAT ; :: thesis: x in B . (n + k)
A5: C . (n + k) = (A . (n + k)) /\ (B . (n + k)) by A1;
x in C . (n + k) by A2;
hence x in B . (n + k) by A5, XBOOLE_0:def 4; :: thesis: verum

end;

then x in lim_inf B by Th7;
hence x in (lim_inf A) /\ (lim_inf B) by A4, XBOOLE_0:def 4; :: thesis: verum

end;

thus (lim_inf A) /\ (lim_inf B) c= lim_inf C :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (lim_inf A) /\ (lim_inf B) or x in lim_inf C )
assume x in (lim_inf A) /\ (lim_inf B) ; :: thesis: x in lim_inf C
then A6: ( x in lim_inf A & x in lim_inf B ) by XBOOLE_0:def 4;
then consider n1 being Element of NAT such that
A7: for k being Element of NAT holds x in A . (n1 + k) by Th7;
consider n2 being Element of NAT such that
A8: for k being Element of NAT holds x in B . (n2 + k) by A6, Th7;
set n = max n1,n2;
A9: for k being Element of NAT holds x in A . ((max n1,n2) + k)

proof

let k be Element of NAT ; :: thesis: x in A . ((max n1,n2) + k)
consider g being Nat such that
A10: max n1,n2 = n1 + g by NAT_1:10, XXREAL_0:25;
reconsider g = g as Element of NAT by ORDINAL1:def 13;
x in A . (n1 + (g + k)) by A7;
hence x in A . ((max n1,n2) + k) by A10; :: thesis: verum

end;

A11: for k being Element of NAT holds x in B . ((max n1,n2) + k)

proof

let k be Element of NAT ; :: thesis: x in B . ((max n1,n2) + k)
consider g being Nat such that
A12: max n1,n2 = n2 + g by NAT_1:10, XXREAL_0:25;
reconsider g = g as Element of NAT by ORDINAL1:def 13;
x in B . (n2 + (g + k)) by A8;
hence x in B . ((max n1,n2) + k) by A12; :: thesis: verum

end;

for k being Element of NAT holds x in C . ((max n1,n2) + k)

proof

let k be Element of NAT ; :: thesis: x in C . ((max n1,n2) + k)
A13: x in A . ((max n1,n2) + k) by A9;
x in B . ((max n1,n2) + k) by A11;
then x in (A . ((max n1,n2) + k)) /\ (B . ((max n1,n2) + k)) by A13, XBOOLE_0:def 4;
hence x in C . ((max n1,n2) + k) by A1; :: thesis: verum

end;

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

end;