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

Intersection (superior_setsequence B) = Union B

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

assume A1: B is V56() ; :: thesis: Intersection (superior_setsequence B) = Union B

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

Intersection (superior_setsequence B) = Union B

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

assume A1: B is V56() ; :: thesis: Intersection (superior_setsequence B) = Union B

now :: thesis: for x being object st x in Intersection (superior_setsequence B) holds

x in Union B

then A3:
Intersection (superior_setsequence B) c= Union B
;x in Union B

let x be object ; :: thesis: ( x in Intersection (superior_setsequence B) implies x in Union B )

assume A2: x in Intersection (superior_setsequence B) ; :: thesis: x in Union B

end;assume A2: x in Intersection (superior_setsequence B) ; :: thesis: x in Union B

now :: thesis: for n being Nat holds x in Union B

hence
x in Union B
; :: thesis: verumlet n be Nat; :: thesis: x in Union B

(superior_setsequence B) . n = Union B by A1, Th42;

hence x in Union B by A2, PROB_1:13; :: thesis: verum

end;(superior_setsequence B) . n = Union B by A1, Th42;

hence x in Union B by A2, PROB_1:13; :: thesis: verum

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

y in Intersection (superior_setsequence B)

then
Union B c= Intersection (superior_setsequence B)
;y in Intersection (superior_setsequence B)

let y be object ; :: thesis: ( y in Union B implies y in Intersection (superior_setsequence B) )

assume y in Union B ; :: thesis: y in Intersection (superior_setsequence B)

then for n being Nat holds y in (superior_setsequence B) . n by A1, Th42;

hence y in Intersection (superior_setsequence B) by PROB_1:13; :: thesis: verum

end;assume y in Union B ; :: thesis: y in Intersection (superior_setsequence B)

then for n being Nat holds y in (superior_setsequence B) . n by A1, Th42;

hence y in Intersection (superior_setsequence B) by PROB_1:13; :: thesis: verum

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