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 \ ((Complement A1) . n) = A1 . n

( x in X & not x in (Complement A1) . n ) ) iff for n being Nat holds x in A1 . n )

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

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 \ ((Complement A1) . n) = A1 . n

proof

A2:
( ( for n being Nat holds
let n be Nat; :: thesis: X \ ((Complement A1) . n) = A1 . n

X \ ((Complement A1) . n) = ((A1 . n) `) ` by Def2

.= A1 . n ;

hence X \ ((Complement A1) . n) = A1 . n ; :: thesis: verum

end;X \ ((Complement A1) . n) = ((A1 . n) `) ` by Def2

.= A1 . n ;

hence X \ ((Complement A1) . n) = A1 . n ; :: thesis: verum

( x in X & not x in (Complement A1) . n ) ) iff for n being Nat holds x in A1 . n )

proof

( x in X & not x in Union (Complement A1) iff ( x in X & ( for n being Nat holds not x in (Complement A1) . n ) ) )
by Th12;
thus
( ( for n being Nat holds

( x in X & not x in (Complement A1) . 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 (Complement A1) . n ) )

( x in X & not x in (Complement A1) . n )

let n be 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;( x in X & not x in (Complement A1) . 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 (Complement A1) . n ) )

proof

assume A4:
for n being Nat holds x in A1 . n
; :: thesis: for n being Nat holds
assume A3:
for n being Nat holds

( x in X & not x in (Complement A1) . n ) ; :: thesis: for n being Nat holds x in A1 . n

let n be Nat; :: thesis: x in A1 . n

not x in (Complement A1) . n by A3;

then x in X \ ((Complement A1) . n) by A3, XBOOLE_0:def 5;

hence x in A1 . n by A1; :: thesis: verum

end;( x in X & not x in (Complement A1) . n ) ; :: thesis: for n being Nat holds x in A1 . n

let n be Nat; :: thesis: x in A1 . n

not x in (Complement A1) . n by A3;

then x in X \ ((Complement A1) . n) by A3, XBOOLE_0:def 5;

hence x in A1 . n by A1; :: thesis: verum

( x in X & not x in (Complement A1) . n )

let n be 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

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