let MySigmaField, MySet be set ; for A1 being SetSequence of MySet st MySet = {1,2,3,4} & rng A1 c= MySigmaField & MySigmaField = {{},{1,2,3,4}} & Intersection A1 <> {} holds
Intersection A1 in MySigmaField
let A1 be SetSequence of MySet; ( MySet = {1,2,3,4} & rng A1 c= MySigmaField & MySigmaField = {{},{1,2,3,4}} & Intersection A1 <> {} implies Intersection A1 in MySigmaField )
assume A0:
( MySet = {1,2,3,4} & rng A1 c= MySigmaField & MySigmaField = {{},{1,2,3,4}} )
; ( not Intersection A1 <> {} or Intersection A1 in MySigmaField )
assume A5:
Intersection A1 <> {}
; Intersection A1 in MySigmaField
D1:
dom A1 = NAT
by FUNCT_2:def 1;
A4:
for n being Nat holds
( A1 . n = {} or A1 . n = {1,2,3,4} )
H1:
( ex n being Nat st A1 . n = {} implies Intersection A1 = {} )
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 ;
( x in Intersection A1 iff x in {1,2,3,4} )
(
x in Intersection A1 iff for
n being
Nat holds
x in {1,2,3,4} )
proof
thus
(
x in Intersection A1 implies for
n being
Nat holds
x in {1,2,3,4} )
( ( for n being Nat holds x in {1,2,3,4} ) implies x in Intersection A1 )proof
assume G1:
x in Intersection A1
;
for n being Nat holds x in {1,2,3,4}
for
n being
Nat holds
x in {1,2,3,4}
proof
let n be
Nat;
x in {1,2,3,4}
for
x being
object holds
(
x in A1 . n iff
x in {1,2,3,4} )
by H1, A4, A5;
hence
x in {1,2,3,4}
by PROB_1:13, G1;
verum
end;
hence
for
n being
Nat holds
x in {1,2,3,4}
;
verum
end;
assume G1:
for
n being
Nat holds
x in {1,2,3,4}
;
x in Intersection A1
for
n being
Nat holds
x in A1 . n
hence
x in Intersection A1
by PROB_1:13;
verum
end;
hence
(
x in Intersection A1 iff
x in {1,2,3,4} )
;
verum
end;
hence
Intersection A1 = {1,2,3,4}
by TARSKI:def 3;
verum
end;
hence
Intersection A1 in MySigmaField
by A0, TARSKI:def 2; verum