let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for A being SetSequence of Sigma
for n being Nat holds . n = (() . n) `

let Sigma be SigmaField of Omega; :: thesis: for A being SetSequence of Sigma
for n being Nat holds . n = (() . n) `

let A be SetSequence of Sigma; :: thesis: for n being Nat holds . n = (() . n) `
let n be Nat; :: thesis: . n = (() . n) `
for x being object holds
( x in . n iff x in (() . n) ` )
proof
let x be object ; :: thesis: ( x in . n iff x in (() . n) ` )
hereby :: thesis: ( x in (() . n) ` implies x in . n )
assume A1: x in . n ; :: thesis: x in (() . n) `
for knat being Nat st knat <= n holds
not x in A . knat
proof
let knat be Nat; :: thesis: ( knat <= n implies not x in A . knat )
assume knat <= n ; :: thesis: not x in A . knat
then A2: x in () . knat by ;
reconsider knat = knat as Element of NAT by ORDINAL1:def 12;
(Complement A) . knat = (A . knat) ` by PROB_1:def 2;
then (Complement A) . knat = Omega \ (A . knat) by SUBSET_1:def 4;
hence not x in A . knat by ; :: thesis: verum
end;
then A3: not x in () . n by PROB_3:26;
x in Omega \ (() . n) by ;
hence x in (() . n) ` by SUBSET_1:def 4; :: thesis: verum
end;
assume A4: x in (() . n) ` ; :: thesis: x in . n
x in Omega \ (() . n) by ;
then A5: ( x in Omega & not x in () . n ) by XBOOLE_0:def 5;
for knat being Nat st knat <= n holds
x in () . knat
proof
let knat be Nat; :: thesis: ( knat <= n implies x in () . knat )
assume knat <= n ; :: thesis: x in () . knat
then ( x in Omega & not x in A . knat ) by ;
then A6: x in Omega \ (A . knat) by XBOOLE_0:def 5;
reconsider knat = knat as Element of NAT by ORDINAL1:def 12;
x in (A . knat) ` by ;
hence x in () . knat by PROB_1:def 2; :: thesis: verum
end;
hence x in . n by PROB_3:25; :: thesis: verum
end;
hence (Partial_Intersection ()) . n = (() . n) ` by TARSKI:2; :: thesis: verum