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
now :: thesis: for x being object st x in Intersection (superior_setsequence B) holds
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
now :: thesis: for n being Nat holds x in Union B
let 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;
hence x in Union B ; :: thesis: verum
end;
then A3: Intersection (superior_setsequence B) c= Union B ;
now :: thesis: for y being object st y in Union B holds
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;
then Union B c= Intersection (superior_setsequence B) ;
hence Intersection (superior_setsequence B) = Union B by A3, XBOOLE_0:def 10; :: thesis: verum