let MyOmega be set ; :: thesis: for A1 being SetSequence of {1,2,3,4} st rng A1 c= MyOmega & MyOmega = {{},{1,2},{3,4},{1,2,3,4}} holds
Intersection A1 in MyOmega
let A1 be SetSequence of {1,2,3,4}; :: thesis: ( rng A1 c= MyOmega & MyOmega = {{},{1,2},{3,4},{1,2,3,4}} implies Intersection A1 in MyOmega )
assume A0: ( rng A1 c= MyOmega & MyOmega = {{},{1,2},{3,4},{1,2,3,4}} ) ; :: thesis: Intersection A1 in MyOmega
Intersection A1 in {{},{1,2},{3,4},{1,2,3,4}}

proof

per cases ( ex n, k being Nat st (A1 . n) /\ (A1 . k) = {} or for n, k being Nat holds not (A1 . n) /\ (A1 . k) = {} ) ;

suppose CASE000: ex n, k being Nat st (A1 . n) /\ (A1 . k) = {} ; :: thesis: Intersection A1 in {{},{1,2},{3,4},{1,2,3,4}}

CASE0: ex n, k being Nat st A1 . n misses A1 . k

proof

consider n, k being Nat such that
BCASE0: (A1 . n) /\ (A1 . k) = {} by CASE000;
A1 . n misses A1 . k by BCASE0;
hence ex n, k being Nat st A1 . n misses A1 . k ; :: thesis: verum

end;

CASE1: for y being object holds
( ( for n, k being Nat holds
( y in A1 . k & y in A1 . n ) ) iff y in {} )

proof

let y be object ; :: thesis: ( ( for n, k being Nat holds
( y in A1 . k & y in A1 . n ) ) iff y in {} )
( ( for n, k being Nat holds
( y in A1 . k & y in A1 . n ) ) implies y in {} )

proof

assume G1: for n, k being Nat holds
( y in A1 . k & y in A1 . n ) ; :: thesis: y in {}
ex n, k being Nat st
( y in A1 . k & y in A1 . n & y in {} )

proof

consider n, k being Nat such that
H1: A1 . n misses A1 . k by CASE0;
( ( y in A1 . k & y in A1 . n ) iff y in {} ) by H1, XBOOLE_0:3;
hence ex n, k being Nat st
( y in A1 . k & y in A1 . n & y in {} ) by G1; :: thesis: verum

end;

hence y in {} ; :: thesis: verum

end;

hence ( ( for n, k being Nat holds
( y in A1 . k & y in A1 . n ) ) iff y in {} ) ; :: thesis: verum

end;

Intersection A1 c= {}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Intersection A1 or y in {} )
( y in Intersection A1 iff for n, k being Nat holds
( y in A1 . k & y in A1 . n ) ) by PROB_1:13;
hence ( not y in Intersection A1 or y in {} ) by CASE1; :: thesis: verum

end;

then Intersection A1 = {} ;
hence Intersection A1 in {{},{1,2},{3,4},{1,2,3,4}} by ENUMSET1:def 2; :: thesis: verum

end;

suppose CASE0: for n, k being Nat holds not (A1 . n) /\ (A1 . k) = {} ; :: thesis: Intersection A1 in {{},{1,2},{3,4},{1,2,3,4}}

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

proof

( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} ) by CASE0, A0, Lm700000;
hence Intersection A1 in {{},{1,2},{3,4},{1,2,3,4}} by ENUMSET1:def 2; :: thesis: verum

end;

hence Intersection A1 in {{},{1,2},{3,4},{1,2,3,4}} ; :: thesis: verum

end;

end;

end;

hence Intersection A1 in MyOmega by A0; :: thesis: verum