let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for A being SetSequence of Sigma

for n being Nat holds (Partial_Intersection (Complement A)) . n = ((Partial_Union A) . n) `

let Sigma be SigmaField of Omega; :: thesis: for A being SetSequence of Sigma

for n being Nat holds (Partial_Intersection (Complement A)) . n = ((Partial_Union A) . n) `

let A be SetSequence of Sigma; :: thesis: for n being Nat holds (Partial_Intersection (Complement A)) . n = ((Partial_Union A) . n) `

let n be Nat; :: thesis: (Partial_Intersection (Complement A)) . n = ((Partial_Union A) . n) `

for x being object holds

( x in (Partial_Intersection (Complement A)) . n iff x in ((Partial_Union A) . n) ` )

for A being SetSequence of Sigma

for n being Nat holds (Partial_Intersection (Complement A)) . n = ((Partial_Union A) . n) `

let Sigma be SigmaField of Omega; :: thesis: for A being SetSequence of Sigma

for n being Nat holds (Partial_Intersection (Complement A)) . n = ((Partial_Union A) . n) `

let A be SetSequence of Sigma; :: thesis: for n being Nat holds (Partial_Intersection (Complement A)) . n = ((Partial_Union A) . n) `

let n be Nat; :: thesis: (Partial_Intersection (Complement A)) . n = ((Partial_Union A) . n) `

for x being object holds

( x in (Partial_Intersection (Complement A)) . n iff x in ((Partial_Union A) . n) ` )

proof

hence
(Partial_Intersection (Complement A)) . n = ((Partial_Union A) . n) `
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in (Partial_Intersection (Complement A)) . n iff x in ((Partial_Union A) . n) ` )

x in Omega \ ((Partial_Union A) . n) by A4, SUBSET_1:def 4;

then A5: ( x in Omega & not x in (Partial_Union A) . n ) by XBOOLE_0:def 5;

for knat being Nat st knat <= n holds

x in (Complement A) . knat

end;hereby :: thesis: ( x in ((Partial_Union A) . n) ` implies x in (Partial_Intersection (Complement A)) . n )

assume A4:
x in ((Partial_Union A) . n) `
; :: thesis: x in (Partial_Intersection (Complement A)) . nassume A1:
x in (Partial_Intersection (Complement A)) . n
; :: thesis: x in ((Partial_Union A) . n) `

for knat being Nat st knat <= n holds

not x in A . knat

x in Omega \ ((Partial_Union A) . n) by A1, A3, XBOOLE_0:def 5;

hence x in ((Partial_Union A) . n) ` by SUBSET_1:def 4; :: thesis: verum

end;for knat being Nat st knat <= n holds

not x in A . knat

proof

then A3:
not x in (Partial_Union A) . n
by PROB_3:26;
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 (Complement A) . knat by A1, PROB_3:25;

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 A2, XBOOLE_0:def 5; :: thesis: verum

end;assume knat <= n ; :: thesis: not x in A . knat

then A2: x in (Complement A) . knat by A1, PROB_3:25;

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 A2, XBOOLE_0:def 5; :: thesis: verum

x in Omega \ ((Partial_Union A) . n) by A1, A3, XBOOLE_0:def 5;

hence x in ((Partial_Union A) . n) ` by SUBSET_1:def 4; :: thesis: verum

x in Omega \ ((Partial_Union A) . n) by A4, SUBSET_1:def 4;

then A5: ( x in Omega & not x in (Partial_Union A) . n ) by XBOOLE_0:def 5;

for knat being Nat st knat <= n holds

x in (Complement A) . knat

proof

hence
x in (Partial_Intersection (Complement A)) . n
by PROB_3:25; :: thesis: verum
let knat be Nat; :: thesis: ( knat <= n implies x in (Complement A) . knat )

assume knat <= n ; :: thesis: x in (Complement A) . knat

then ( x in Omega & not x in A . knat ) by A5, PROB_3:26;

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 A6, SUBSET_1:def 4;

hence x in (Complement A) . knat by PROB_1:def 2; :: thesis: verum

end;assume knat <= n ; :: thesis: x in (Complement A) . knat

then ( x in Omega & not x in A . knat ) by A5, PROB_3:26;

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 A6, SUBSET_1:def 4;

hence x in (Complement A) . knat by PROB_1:def 2; :: thesis: verum