let X be set ; :: thesis: for B being SetSequence of X st B is non-descending holds
Intersection (superior_setsequence B) = Union B
let B be SetSequence of X; :: thesis: ( B is non-descending implies Intersection (superior_setsequence B) = Union B )
assume A1: B is non-descending ; :: thesis: Intersection (superior_setsequence B) = Union B

now :: thesis: for x being object st x in Intersection (superior_setsequence B) holds
x in Union B

let x be object ; :: thesis: ( x in Intersection (superior_setsequence B) implies x in Union B )
assume A2: x in Intersection (superior_setsequence B) ; :: thesis: x in Union B

now :: thesis: for n being Nat holds x in Union B

let n be Nat; :: thesis: x in Union B
(superior_setsequence B) . n = Union B by A1, Th42;
hence x in Union B by A2, PROB_1:13; :: thesis: verum

end;

hence x in Union B ; :: thesis: verum

end;

then A3: Intersection (superior_setsequence B) c= Union B ;

now :: thesis: for y being object st y in Union B holds
y in Intersection (superior_setsequence B)

let y be object ; :: thesis: ( y in Union B implies y in Intersection (superior_setsequence B) )
assume y in Union B ; :: thesis: y in Intersection (superior_setsequence B)
then for n being Nat holds y in (superior_setsequence B) . n by A1, Th42;
hence y in Intersection (superior_setsequence B) by PROB_1:13; :: thesis: verum

end;

then Union B c= Intersection (superior_setsequence B) ;
hence Intersection (superior_setsequence B) = Union B by A3, XBOOLE_0:def 10; :: thesis: verum