let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for A being SetSequence of Sigma
for n being Element of 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 Element of NAT holds (@Partial_Intersection (@Complement A)) . n = ((@Partial_Union A) . n) `
let A be SetSequence of Sigma; :: thesis: for n being Element of NAT holds (@Partial_Intersection (@Complement A)) . n = ((@Partial_Union A) . n) `
let n be Element of NAT ; :: thesis: (@Partial_Intersection (@Complement A)) . n = ((@Partial_Union A) . n) `
for x being set holds
( x in (@Partial_Intersection (@Complement A)) . n iff x in ((@Partial_Union A) . n) ` )

proof

let x be set ; :: 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:29;
reconsider knat = knat as Element of NAT by ORDINAL1:def 13;
(@Complement A) . knat = (A . knat) ` by PROB_1:def 4;
then (@Complement A) . knat = Omega \ (A . knat) by SUBSET_1:def 5;
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:30;
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 5; :: 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 5;
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:30;
then A6: x in Omega \ (A . knat) by XBOOLE_0:def 5;
reconsider knat = knat as Element of NAT by ORDINAL1:def 13;
x in (A . knat) ` by A6, SUBSET_1:def 5;
hence x in (@Complement A) . knat by PROB_1:def 4; :: thesis: verum

end;

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

end;

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