let Omega be non empty set ; for f being SetSequence of Omega st f is V62() holds
for X being Subset of Omega holds seqIntersection (X,f) is V62()
let f be SetSequence of Omega; ( f is V62() implies for X being Subset of Omega holds seqIntersection (X,f) is V62() )
assume A1:
f is V62()
; for X being Subset of Omega holds seqIntersection (X,f) is V62()
let X be Subset of Omega; seqIntersection (X,f) is V62()
for n, m being Element of NAT st n < m holds
(seqIntersection (X,f)) . n misses (seqIntersection (X,f)) . m
proof
let n,
m be
Element of
NAT ;
( n < m implies (seqIntersection (X,f)) . n misses (seqIntersection (X,f)) . m )
assume
n < m
;
(seqIntersection (X,f)) . n misses (seqIntersection (X,f)) . m
then
f . n misses f . m
by A1;
then A2:
X /\ (f . n) misses f . m
by XBOOLE_1:74;
(
(seqIntersection (X,f)) . n = X /\ (f . n) &
(seqIntersection (X,f)) . m = X /\ (f . m) )
by Def1;
hence
(seqIntersection (X,f)) . n misses (seqIntersection (X,f)) . m
by A2, XBOOLE_1:74;
verum
end;
hence
seqIntersection (X,f) is V62()
; verum