let A1 be SetSequence of {1,2,3,4}; :: thesis: ( ( for n, k being Nat holds not (A1 . n) /\ (A1 . k) = {} ) & rng A1 c= {{},{1,2},{3,4},{1,2,3,4}} & not Intersection A1 = {} & not Intersection A1 = {1,2} & not Intersection A1 = {3,4} implies Intersection A1 = {1,2,3,4} )
assume GENASS0: ( ( for n, k being Nat holds not (A1 . n) /\ (A1 . k) = {} ) & rng A1 c= {{},{1,2},{3,4},{1,2,3,4}} ) ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} )
set MyOmega = {{},{1,2},{3,4},{1,2,3,4}};
D1: dom A1 = NAT by FUNCT_2:def 1;
S20: for n being Nat holds A1 . n in {{},{1,2},{3,4},{1,2,3,4}}

proof

let n be Nat; :: thesis: A1 . n in {{},{1,2},{3,4},{1,2,3,4}}
n in dom A1 by D1, ORDINAL1:def 12;
hence A1 . n in {{},{1,2},{3,4},{1,2,3,4}} by FUNCT_1:3, GENASS0; :: thesis: verum

end;

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} )

proof

let n be Nat; :: thesis: ( A1 . n = {} or A1 . n = {1,2} or A1 . n = {3,4} or A1 . n = {1,2,3,4} )
A1 . n in {{},{1,2},{3,4},{1,2,3,4}} by S20;
hence ( A1 . n = {} or A1 . n = {1,2} or A1 . n = {3,4} or A1 . n = {1,2,3,4} ) by ENUMSET1:def 2; :: thesis: verum

end;

Fin1: for n being Nat holds Intersection A1 c= A1 . n by PROB_1:13;

per cases ( Intersection A1 = {1,2,3,4} or Intersection A1 <> {1,2,3,4} ) ;

suppose Intersection A1 = {1,2,3,4} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} )

hence ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} ) ; :: thesis: verum

end;

suppose MYSUPP0: Intersection A1 <> {1,2,3,4} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} )

W0: ( Intersection A1 c= {} or Intersection A1 c= {1,2} or Intersection A1 c= {3,4} )

proof

( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} )

proof

per cases ( for n being Nat holds A1 . n = {1,2,3,4} or ex n being Nat st A1 . n <> {1,2,3,4} ) ;

suppose ASS1: for n being Nat holds A1 . n = {1,2,3,4} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} )

Intersection A1 = {1,2,3,4}

proof

for x being object holds
( x in Intersection A1 iff x in {1,2,3,4} )

proof

let x be object ; :: thesis: ( x in Intersection A1 iff x in {1,2,3,4} )
( ( for n being Nat holds x in A1 . n ) iff x in {1,2,3,4} )

proof

( ( for n being Nat holds x in A1 . n ) implies x in {1,2,3,4} )

proof

assume for n being Nat holds x in A1 . n ; :: thesis: x in {1,2,3,4}
then x in A1 . 0 ;
then consider k being Nat such that
N10: x in A1 . k ;
thus x in {1,2,3,4} by N10; :: thesis: verum

end;

hence ( ( for n being Nat holds x in A1 . n ) iff x in {1,2,3,4} ) by ASS1; :: thesis: verum

end;

hence ( x in Intersection A1 iff x in {1,2,3,4} ) by PROB_1:13; :: thesis: verum

end;

hence Intersection A1 = {1,2,3,4} by TARSKI:2; :: thesis: verum

end;

hence ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} ) by MYSUPP0; :: thesis: verum

end;

suppose ex n being Nat st A1 . n <> {1,2,3,4} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} )

then consider n being Nat such that
KK: A1 . n <> {1,2,3,4} ;

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: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} )

hence ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} ) by The1; :: thesis: verum

end;

suppose JSUPP1: A1 . n = {1,2} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} )

( Intersection A1 = {} or Intersection A1 = {1,2} )

proof

per cases ( Intersection A1 = {1,2} or Intersection A1 <> {1,2} ) ;

suppose Intersection A1 = {1,2} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} )

hence ( Intersection A1 = {} or Intersection A1 = {1,2} ) ; :: thesis: verum

end;

suppose Intersection A1 <> {1,2} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} )

then ( Intersection A1 = {1} or Intersection A1 = {2} or Intersection A1 = {} ) by ZFMISC_1:36, JSUPP1, Fin1;
hence ( Intersection A1 = {} or Intersection A1 = {1,2} ) by SuperLemma2, SuperLemma1, S2; :: thesis: verum

end;

end;

end;

hence ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} ) ; :: thesis: verum

end;

suppose SUPP1: A1 . n = {3,4} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} )

( Intersection A1 = {} or Intersection A1 = {3,4} )

proof

per cases ( Intersection A1 = {3,4} or Intersection A1 <> {3,4} ) ;

suppose Intersection A1 = {3,4} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {3,4} )

hence ( Intersection A1 = {} or Intersection A1 = {3,4} ) ; :: thesis: verum

end;

suppose Intersection A1 <> {3,4} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {3,4} )

then ( Intersection A1 = {3} or Intersection A1 = {4} or Intersection A1 = {} ) by SUPP1, Fin1, ZFMISC_1:36;
hence ( Intersection A1 = {} or Intersection A1 = {3,4} ) by SuperLemma1, S2, SuperLemma2; :: thesis: verum

end;

end;

end;

hence ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} ) ; :: thesis: verum

end;

suppose A1 . n = {1,2,3,4} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} )

hence ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} ) by KK; :: thesis: verum

end;

end;

end;

end;

end;

hence ( Intersection A1 c= {} or Intersection A1 c= {1,2} or Intersection A1 c= {3,4} ) ; :: thesis: verum

end;

per cases ( Intersection A1 c= {} or Intersection A1 c= {1,2} or Intersection A1 c= {3,4} ) by W0;

suppose Intersection A1 c= {} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} )

hence ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} ) ; :: thesis: verum

end;

suppose ZW10: Intersection A1 c= {1,2} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} )

per cases ( Intersection A1 = {1,2} or Intersection A1 <> {1,2} ) ;

suppose Intersection A1 = {1,2} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} )

hence ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} ) ; :: thesis: verum

end;

suppose Intersection A1 <> {1,2} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} )

then ( Intersection A1 = {1} or Intersection A1 = {2} or Intersection A1 = {} ) by ZW10, ZFMISC_1:36;
hence ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} ) by SuperLemma1, S2, SuperLemma2; :: thesis: verum

end;

end;

end;

suppose ZW10: Intersection A1 c= {3,4} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} )

per cases ( Intersection A1 = {3,4} or Intersection A1 <> {3,4} ) ;

suppose Intersection A1 = {3,4} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} )

hence ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} ) ; :: thesis: verum

end;

suppose Intersection A1 <> {3,4} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} )

then ( Intersection A1 = {3} or Intersection A1 = {4} or Intersection A1 = {} ) by ZW10, ZFMISC_1:36;
hence ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} ) by SuperLemma1, S2, SuperLemma2; :: thesis: verum

end;

end;

end;

end;

end;

end;