let X be set ; :: thesis: for B being SetSequence of X st B is V55() holds

Union (inferior_setsequence B) = Intersection B

let B be SetSequence of X; :: thesis: ( B is V55() implies Union (inferior_setsequence B) = Intersection B )

assume A1: B is V55() ; :: thesis: Union (inferior_setsequence B) = Intersection B

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

Union (inferior_setsequence B) = Intersection B

let B be SetSequence of X; :: thesis: ( B is V55() implies Union (inferior_setsequence B) = Intersection B )

assume A1: B is V55() ; :: 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

then A2:
Union (inferior_setsequence B) c= Intersection B
;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;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

now :: thesis: for y being object st y in Intersection B holds

y in Union (inferior_setsequence B)

then
Intersection B c= Union (inferior_setsequence B)
;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;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

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