let X be set ; :: thesis: for A1 being SetSequence of X
for x being object holds
( x in Intersection A1 iff for n being Nat holds x in A1 . n )

let A1 be SetSequence of X; :: thesis: for x being object holds
( x in Intersection A1 iff for n being Nat holds x in A1 . n )

let x be object ; :: thesis: ( x in Intersection A1 iff for n being Nat holds x in A1 . n )
A1: for n being Nat holds X \ (() . n) = A1 . n
proof
let n be Nat; :: thesis: X \ (() . n) = A1 . n
X \ (() . n) = ((A1 . n) `) ` by Def2
.= A1 . n ;
hence X \ (() . n) = A1 . n ; :: thesis: verum
end;
A2: ( ( for n being Nat holds
( x in X & not x in () . n ) ) iff for n being Nat holds x in A1 . n )
proof
thus ( ( for n being Nat holds
( x in X & not x in () . n ) ) implies for n being Nat holds x in A1 . n ) :: thesis: ( ( for n being Nat holds x in A1 . n ) implies for n being Nat holds
( x in X & not x in () . n ) )
proof
assume A3: for n being Nat holds
( x in X & not x in () . n ) ; :: thesis: for n being Nat holds x in A1 . n
let n be Nat; :: thesis: x in A1 . n
not x in () . n by A3;
then x in X \ (() . n) by ;
hence x in A1 . n by A1; :: thesis: verum
end;
assume A4: for n being Nat holds x in A1 . n ; :: thesis: for n being Nat holds
( x in X & not x in () . n )

let n be Nat; :: thesis: ( x in X & not x in () . n )
x in A1 . n by A4;
then x in X \ (() . n) by A1;
hence ( x in X & not x in () . n ) by XBOOLE_0:def 5; :: thesis: verum
end;
( x in X & not x in Union () iff ( x in X & ( for n being Nat holds not x in () . n ) ) ) by Th12;
hence ( x in Intersection A1 iff for n being Nat holds x in A1 . n ) by ; :: thesis: verum