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 A00: B is non-descending ; :: thesis: Intersection (superior_setsequence B) = Union B
Intersection (superior_setsequence B) = Union B

proof

now

let x be set ; :: thesis: ( x in Intersection (superior_setsequence B) implies x in Union B )
assume B0: 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 A00, Th31;
hence x in Union B by B0, PROB_1:29; :: thesis: verum

end;

hence x in Union B ; :: thesis: verum

end;

then BB0: 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 C0: y in Union B ; :: thesis: y in Intersection (superior_setsequence B)
for n being Element of NAT holds y in (superior_setsequence B) . n by C0, A00, Th31;
hence y in Intersection (superior_setsequence B) by PROB_1:29; :: thesis: verum

end;

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

end;

hence Intersection (superior_setsequence B) = Union B ; :: thesis: verum