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

proof

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

end;

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