let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X holds lim_inf (A (\/) A1) = A \/ (lim_inf A1)
let A be Subset of X; :: thesis: for A1 being SetSequence of X holds lim_inf (A (\/) A1) = A \/ (lim_inf A1)
let A1 be SetSequence of X; :: thesis: lim_inf (A (\/) A1) = A \/ (lim_inf A1)
reconsider X1 = inferior_setsequence A1 as SetSequence of X ;
reconsider X2 = inferior_setsequence (A (\/) A1) as SetSequence of X ;
X2 = A (\/) X1

proof

let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: X2 . n = (A (\/) X1) . n
thus X2 . n = A \/ (X1 . n) by Th51
.= (A (\/) X1) . n by Def6 ; :: thesis: verum

end;

then Union X2 = A \/ (Union X1) by Th39;
then lim_inf (A (\/) A1) = A \/ (Union X1) by SETLIM_1:def 4;
hence lim_inf (A (\/) A1) = A \/ (lim_inf A1) by SETLIM_1:def 4; :: thesis: verum