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

proof

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 consider k being Element of NAT such that
B0: x in (inferior_setsequence B) . k by PROB_1:25;
thus x in Intersection B by A00, B0, Th41; :: thesis: verum

end;

then BB0: 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 Th19;
hence y in Union (inferior_setsequence B) by PROB_1:25; :: thesis: verum

end;

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

end;

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