let X, x be set ; :: thesis: for A1 being SetSequence of X holds
( x in Intersection A1 iff for n being Element of NAT holds x in A1 . n )
let A1 be SetSequence of X; :: thesis: ( x in Intersection A1 iff for n being Element of NAT holds x in A1 . n )
A1: for n being Element of NAT holds X \ ((Complement A1) . n) = A1 . n

proof

let n be Element of NAT ; :: thesis: X \ ((Complement A1) . n) = A1 . n
X \ ((Complement A1) . n) = ((A1 . n) ` ) ` by Def4
.= A1 . n ;
hence X \ ((Complement A1) . n) = A1 . n ; :: thesis: verum

end;

A2: ( x in X & not x in Union (Complement A1) iff ( x in X & ( for n being Element of NAT holds not x in (Complement A1) . n ) ) ) by Th25;
( ( for n being Element of NAT holds
( x in X & not x in (Complement A1) . n ) ) iff for n being Element of NAT holds x in A1 . n )

proof

thus ( ( for n being Element of NAT holds
( x in X & not x in (Complement A1) . n ) ) implies for n being Element of NAT holds x in A1 . n ) :: thesis: ( ( for n being Element of NAT holds x in A1 . n ) implies for n being Element of NAT holds
( x in X & not x in (Complement A1) . n ) )

proof

assume A3: for n being Element of NAT holds
( x in X & not x in (Complement A1) . n ) ; :: thesis: for n being Element of NAT holds x in A1 . n
let n be Element of NAT ; :: thesis: x in A1 . n
( x in X & not x in (Complement A1) . n ) by A3;
then x in X \ ((Complement A1) . n) by XBOOLE_0:def 5;
hence x in A1 . n by A1; :: thesis: verum

end;

assume A4: for n being Element of NAT holds x in A1 . n ; :: thesis: for n being Element of NAT holds
( x in X & not x in (Complement A1) . n )
let n be Element of NAT ; :: thesis: ( x in X & not x in (Complement A1) . n )
x in A1 . n by A4;
then x in X \ ((Complement A1) . n) by A1;
hence ( x in X & not x in (Complement A1) . n ) by XBOOLE_0:def 5; :: thesis: verum

end;

hence ( x in Intersection A1 iff for n being Element of NAT holds x in A1 . n ) by A2, XBOOLE_0:def 5; :: thesis: verum