let X be set ; :: thesis: for Si being SigmaField of X
for S1, S2, S3 being SetSequence of Si st ( for n being Nat holds S3 . n = (S1 . n) /\ (S2 . n) ) holds
lim_inf S3 = (lim_inf S1) /\ (lim_inf S2)
let Si be SigmaField of X; :: thesis: for S1, S2, S3 being SetSequence of Si st ( for n being Nat holds S3 . n = (S1 . n) /\ (S2 . n) ) holds
lim_inf S3 = (lim_inf S1) /\ (lim_inf S2)
let S1, S2, S3 be SetSequence of Si; :: thesis: ( ( for n being Nat holds S3 . n = (S1 . n) /\ (S2 . n) ) implies lim_inf S3 = (lim_inf S1) /\ (lim_inf S2) )
A1: for B, A2, A3 being SetSequence of X st ( for n being Nat holds A3 . n = (B . n) /\ (A2 . n) ) holds
(Union (inferior_setsequence B)) /\ (Union (inferior_setsequence A2)) = Union (inferior_setsequence A3)

proof

let B, A2, A3 be SetSequence of X; :: thesis: ( ( for n being Nat holds A3 . n = (B . n) /\ (A2 . n) ) implies (Union (inferior_setsequence B)) /\ (Union (inferior_setsequence A2)) = Union (inferior_setsequence A3) )
A2: ( lim_inf B = Union (inferior_setsequence B) & lim_inf A2 = Union (inferior_setsequence A2) ) ;
A3: lim_inf A3 = Union (inferior_setsequence A3) ;
assume for n being Nat holds A3 . n = (B . n) /\ (A2 . n) ; :: thesis: (Union (inferior_setsequence B)) /\ (Union (inferior_setsequence A2)) = Union (inferior_setsequence A3)
hence (Union (inferior_setsequence B)) /\ (Union (inferior_setsequence A2)) = Union (inferior_setsequence A3) by A2, A3, KURATO_0:10; :: thesis: verum

end;

assume for n being Nat holds S3 . n = (S1 . n) /\ (S2 . n) ; :: thesis: lim_inf S3 = (lim_inf S1) /\ (lim_inf S2)
hence lim_inf S3 = (lim_inf S1) /\ (lim_inf S2) by A1; :: thesis: verum