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) ` )

proof

let x be object ; :: thesis: ( x in (Partial_Intersection (Complement A)) . n iff x in ((Partial_Union A) . n) ` )

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

assume 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

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 (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;

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

assume A4: x in ((Partial_Union A) . n) ` ; :: thesis: x in (Partial_Intersection (Complement 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

proof

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;

hence x in (Partial_Intersection (Complement A)) . n by PROB_3:25; :: thesis: verum

end;

hence (Partial_Intersection (Complement A)) . n = ((Partial_Union A) . n) ` by TARSKI:2; :: thesis: verum