let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X holds lim_sup (A (/\) A1) = A /\ (lim_sup A1)
let A be Subset of X; :: thesis: for A1 being SetSequence of X holds lim_sup (A (/\) A1) = A /\ (lim_sup A1)
let A1 be SetSequence of X; :: thesis: lim_sup (A (/\) A1) = A /\ (lim_sup A1)
reconsider X1 = superior_setsequence A1 as SetSequence of X ;
reconsider X2 = superior_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 Th55
.= (A (/\) X1) . n by Def5 ; :: thesis: verum

end;

then Intersection X2 = A /\ (Intersection X1) by Th33;
then lim_sup (A (/\) A1) = A /\ (Intersection X1) by SETLIM_1:def 5;
hence lim_sup (A (/\) A1) = A /\ (lim_sup A1) by SETLIM_1:def 5; :: thesis: verum