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

now

let x be set ; :: thesis: ( x in Union (inferior_setsequence B) implies x in Intersection B )
assume x in Union (inferior_setsequence B) ; :: thesis: x in Intersection B
then ex k being Element of NAT st x in (inferior_setsequence B) . k by PROB_1:12;
hence x in Intersection B by A1, Th52; :: thesis: verum

end;

then A2: Union (inferior_setsequence B) c= Intersection B by TARSKI:def 3;

now

let y be set ; :: thesis: ( y in Intersection B implies y in Union (inferior_setsequence B) )
assume y in Intersection B ; :: thesis: y in Union (inferior_setsequence B)
then y in (inferior_setsequence B) . 0 by Th17;
hence y in Union (inferior_setsequence B) by PROB_1:12; :: thesis: verum

end;

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