let MyOmega be set ; 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}; ( 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}} )
; 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) = {}
;
Intersection A1 in {{},{1,2},{3,4},{1,2,3,4}}CASE0:
ex
n,
k being
Nat st
A1 . n misses A1 . k
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 ;
( ( 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 {} )
hence
( ( for
n,
k being
Nat holds
(
y in A1 . k &
y in A1 . n ) ) iff
y in {} )
;
verum
end;
Intersection A1 c= {}
then
Intersection A1 = {}
;
hence
Intersection A1 in {{},{1,2},{3,4},{1,2,3,4}}
by ENUMSET1:def 2;
verum end; suppose CASE0:
for
n,
k being
Nat holds not
(A1 . n) /\ (A1 . k) = {}
;
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;
verum
end; hence
Intersection A1 in {{},{1,2},{3,4},{1,2,3,4}}
;
verum end; end;
end;
hence
Intersection A1 in MyOmega
by A0; verum