let A1 be SetSequence of {1,2,3,4}; :: thesis:
let w be Real; :: thesis:
assume KX: ( w = 2 or w = 4 ) ; :: thesis:
assume S2: for n being Nat holds
( A1 . n = {} or A1 . n = {1,2} or A1 . n = {3,4} or A1 . n = {1,2,3,4} ) ; :: thesis:

per cases ;

suppose Intersection A1 = {} ; :: thesis:

hence {w} <> Intersection A1 ; :: thesis:

end;

suppose SUPP1: Intersection A1 <> {} ; :: thesis:

ex x being object st
( ( for n being Nat holds x in A1 . n ) & not x in {w} )

proof

per cases ;

suppose ex j being Nat st A1 . j = {} ; :: thesis:

then consider j being Nat such that
J0: A1 . j = {} ;
thus ex x being object st
( ( for n being Nat holds x in A1 . n ) & not x in {w} ) by The1, J0, SUPP1; :: thesis:

end;

suppose USUPP1: for n being Nat holds A1 . n <> {} ; :: thesis:

per cases ;

suppose P1: for j being Nat holds {1,2} c= A1 . j ; :: thesis:

set x = 1;
Z1: not 1 in {w} by TARSKI:def 1, KX;
for n being Nat holds 1 in A1 . n

proof

let n be Nat; :: thesis:

per cases by S2;

suppose A1 . n = {} ; :: thesis:

hence 1 in A1 . n by USUPP1; :: thesis:

end;

suppose A1 . n = {1,2} ; :: thesis:

hence 1 in A1 . n by TARSKI:def 2; :: thesis:

end;

suppose J0: A1 . n = {3,4} ; :: thesis:

1 in {1,2} by TARSKI:def 2;
then not {1,2} c= A1 . n by J0, TARSKI:def 2;
hence 1 in A1 . n by P1; :: thesis:

end;

suppose A1 . n = {1,2,3,4} ; :: thesis:

hence 1 in A1 . n by ENUMSET1:def 2; :: thesis:

end;

end;

end;

hence ex x being object st
( ( for n being Nat holds x in A1 . n ) & not x in {w} ) by Z1; :: thesis:

end;

suppose not for j being Nat holds {1,2} c= A1 . j ; :: thesis:

then consider j being Nat such that
BSUPP1: not {1,2} c= A1 . j ;

per cases ;

suppose P1: for n being Nat holds {3,4} c= A1 . n ; :: thesis:

set x = 3;
Z1: not 3 in {w} by TARSKI:def 1, KX;
for n being Nat holds 3 in A1 . n

proof

let n be Nat; :: thesis:

per cases by S2;

suppose A1 . n = {} ; :: thesis:

hence 3 in A1 . n by USUPP1; :: thesis:

end;

suppose A1 . n = {3,4} ; :: thesis:

hence 3 in A1 . n by TARSKI:def 2; :: thesis:

end;

suppose J0: A1 . n = {1,2} ; :: thesis:

3 in {3,4} by TARSKI:def 2;
then not {3,4} c= A1 . n by J0, TARSKI:def 2;
hence 3 in A1 . n by P1; :: thesis:

end;

suppose A1 . n = {1,2,3,4} ; :: thesis:

hence 3 in A1 . n by ENUMSET1:def 2; :: thesis:

end;

end;

end;

hence ex x being object st
( ( for n being Nat holds x in A1 . n ) & not x in {w} ) by Z1; :: thesis:

end;

suppose not for k being Nat holds {3,4} c= A1 . k ; :: thesis:

then consider k being Nat such that
CSUPP1: not {3,4} c= A1 . k ;
ZW1: (A1 . k) /\ (A1 . j) = {}

proof

per cases by S2, Lm2, BSUPP1;

suppose DSUPP1: A1 . j = {3,4} ; :: thesis:

per cases by CSUPP1, Lm1, S2;

suppose A1 . k = {1,2} ; :: thesis:

hence (A1 . k) /\ (A1 . j) = {} by Lm3, DSUPP1; :: thesis:

end;

suppose A1 . k = {} ; :: thesis:

hence (A1 . k) /\ (A1 . j) = {} ; :: thesis:

end;

end;

end;

suppose A1 . j = {} ; :: thesis:

hence (A1 . k) /\ (A1 . j) = {} ; :: thesis:

end;

end;

end;

Intersection A1 = {}

proof

Intersection A1 c= (A1 . k) /\ (A1 . j)

proof

for x being object st x in Intersection A1 holds
x in (A1 . k) /\ (A1 . j)

proof

let x be object ; :: thesis:
assume x in Intersection A1 ; :: thesis:
then ( x in A1 . k & x in A1 . j ) by PROB_1:13;
hence x in (A1 . k) /\ (A1 . j) by XBOOLE_0:def 4; :: thesis:

end;

hence Intersection A1 c= (A1 . k) /\ (A1 . j) ; :: thesis:

end;

hence Intersection A1 = {} by ZW1; :: thesis:

end;

hence ex x being object st
( ( for n being Nat holds x in A1 . n ) & not x in {w} ) by SUPP1; :: thesis:

end;

end;

end;

end;

end;

end;

end;

hence {w} <> Intersection A1 by PROB_1:13; :: thesis:

end;

end;