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