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

let x be set ; :: 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

let n be Element of 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 by TARSKI:def 3;

now

let y be set ; :: 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 Element of 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) by TARSKI:def 3;
hence Intersection (superior_setsequence B) = Union B by A3, XBOOLE_0:def 10; :: thesis: verum