let A1 be SetSequence of {1,2,3,4}; :: thesis: for w being Real st ( w = 1 or w = 3 ) & ( for n being Nat holds
( A1 . n = {} or A1 . n = {1,2} or A1 . n = {3,4} or A1 . n = {1,2,3,4} ) ) holds
{w} <> Intersection A1
let w be Real; :: thesis: ( ( w = 1 or w = 3 ) & ( for n being Nat holds
( A1 . n = {} or A1 . n = {1,2} or A1 . n = {3,4} or A1 . n = {1,2,3,4} ) ) implies {w} <> Intersection A1 )
assume KX: ( w = 1 or w = 3 ) ; :: thesis: ( ex n being Nat st
( not A1 . n = {} & not A1 . n = {1,2} & not A1 . n = {3,4} & not A1 . n = {1,2,3,4} ) or {w} <> Intersection A1 )
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: {w} <> Intersection A1
per cases ( Intersection A1 = {} or Intersection A1 <> {} ) ;
suppose Intersection A1 = {} ; :: thesis: {w} <> Intersection A1
hence {w} <> Intersection A1 ; :: thesis: verum
end;
suppose SUPP1: Intersection A1 <> {} ; :: thesis: {w} <> Intersection A1
ex x being object st
( ( for n being Nat holds x in A1 . n ) & not x in {w} )
proof
per cases ( ex j being Nat st A1 . j = {} or for n being Nat holds A1 . n <> {} ) ;
suppose ex j being Nat st A1 . j = {} ; :: thesis: ex x being object st
( ( for n being Nat holds x in A1 . n ) & not x in {w} )
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: verum
end;
suppose USUPP1: for n being Nat holds A1 . n <> {} ; :: thesis: ex x being object st
( ( for n being Nat holds x in A1 . n ) & not x in {w} )
per cases ( for j being Nat holds {1,2} c= A1 . j or ex j being Nat st not {1,2} c= A1 . j ) ;
suppose P1: for j being Nat holds {1,2} c= A1 . j ; :: thesis: ex x being object st
( ( for n being Nat holds x in A1 . n ) & not x in {w} )
set x = 2;
Z1: not 2 in {w} by TARSKI:def 1, KX;
for n being Nat holds 2 in A1 . n
proof
let n be Nat; :: thesis: 2 in A1 . n
per cases ( A1 . n = {} or A1 . n = {1,2} or A1 . n = {3,4} or A1 . n = {1,2,3,4} ) by S2;
suppose A1 . n = {} ; :: thesis: 2 in A1 . n
hence 2 in A1 . n by USUPP1; :: thesis: verum
end;
suppose A1 . n = {1,2} ; :: thesis: 2 in A1 . n
hence 2 in A1 . n by TARSKI:def 2; :: thesis: verum
end;
suppose J0: A1 . n = {3,4} ; :: thesis: 2 in A1 . n
2 in {1,2} by TARSKI:def 2;
then not {1,2} c= A1 . n by J0, TARSKI:def 2;
hence 2 in A1 . n by P1; :: thesis: verum
end;
suppose A1 . n = {1,2,3,4} ; :: thesis: 2 in A1 . n
hence 2 in A1 . n by ENUMSET1:def 2; :: thesis: verum
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: verum
end;
suppose not for j being Nat holds {1,2} c= A1 . j ; :: thesis: ex x being object st
( ( for n being Nat holds x in A1 . n ) & not x in {w} )
then consider j being Nat such that
BSUPP1: not {1,2} c= A1 . j ;
per cases ( for n being Nat holds {3,4} c= A1 . n or ex k being Nat st not {3,4} c= A1 . k ) ;
suppose P1: for n being Nat holds {3,4} c= A1 . n ; :: thesis: ex x being object st
( ( for n being Nat holds x in A1 . n ) & not x in {w} )
set x = 4;
Z1: not 4 in {w} by TARSKI:def 1, KX;
for n being Nat holds 4 in A1 . n
proof
let n be Nat; :: thesis: 4 in A1 . n
per cases ( A1 . n = {} or A1 . n = {3,4} or A1 . n = {1,2} or A1 . n = {1,2,3,4} ) by S2;
suppose A1 . n = {} ; :: thesis: 4 in A1 . n
hence 4 in A1 . n by USUPP1; :: thesis: verum
end;
suppose A1 . n = {3,4} ; :: thesis: 4 in A1 . n
hence 4 in A1 . n by TARSKI:def 2; :: thesis: verum
end;
suppose J0: A1 . n = {1,2} ; :: thesis: 4 in A1 . n
4 in {3,4} by TARSKI:def 2;
then not {3,4} c= A1 . n by J0, TARSKI:def 2;
hence 4 in A1 . n by P1; :: thesis: verum
end;
suppose A1 . n = {1,2,3,4} ; :: thesis: 4 in A1 . n
hence 4 in A1 . n by ENUMSET1:def 2; :: thesis: verum
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: verum
end;
suppose not for k being Nat holds {3,4} c= A1 . k ; :: thesis: ex x being object st
( ( for n being Nat holds x in A1 . n ) & not x in {w} )
then consider k being Nat such that
CSUPP1: not {3,4} c= A1 . k ;
ZW1: (A1 . k) /\ (A1 . j) = {}
proof
per cases ( A1 . j = {3,4} or A1 . j = {} ) by S2, Lm2, BSUPP1;
suppose DSUPP1: A1 . j = {3,4} ; :: thesis: (A1 . k) /\ (A1 . j) = {}
( A1 . k = {1,2} or A1 . k = {} ) by S2, CSUPP1, Lm1;
hence (A1 . k) /\ (A1 . j) = {} by Lm3, DSUPP1; :: thesis: verum
end;
suppose A1 . j = {} ; :: thesis: (A1 . k) /\ (A1 . j) = {}
hence (A1 . k) /\ (A1 . j) = {} ; :: thesis: verum
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: ( x in Intersection A1 implies x in (A1 . k) /\ (A1 . j) )
assume x in Intersection A1 ; :: thesis: x in (A1 . k) /\ (A1 . j)
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: verum
end;
hence Intersection A1 c= (A1 . k) /\ (A1 . j) ; :: thesis: verum
end;
hence Intersection A1 = {} by ZW1; :: thesis: verum
end;
hence ex x being object st
( ( for n being Nat holds x in A1 . n ) & not x in {w} ) by SUPP1; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
hence {w} <> Intersection A1 by PROB_1:13; :: thesis: verum
end;
end;