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 :: thesis: for x being object st x in Union (inferior_setsequence B) holds
x in Intersection B

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

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

let y be object ; :: 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) ;
hence Union (inferior_setsequence B) = Intersection B by A2, XBOOLE_0:def 10; :: thesis: verum