let n, k be Nat; :: thesis: for Affn being affinely-independent Subset of ()
for Ak being Subset of ()
for EN being Enumeration of Affn
for B being Subset of (() | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of (() | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds
( Ak is closed iff B is closed )

let Affn be affinely-independent Subset of (); :: thesis: for Ak being Subset of ()
for EN being Enumeration of Affn
for B being Subset of (() | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of (() | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds
( Ak is closed iff B is closed )

let Ak be Subset of (); :: thesis: for EN being Enumeration of Affn
for B being Subset of (() | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of (() | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds
( Ak is closed iff B is closed )

let E be Enumeration of Affn; :: thesis: for B being Subset of (() | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of (() | (Affin Affn)) : (pnA |-- E) | k in Ak } holds
( Ak is closed iff B is closed )

set TRn = TOP-REAL n;
set A = Affn;
set AA = Affin Affn;
let B be Subset of (() | (Affin Affn)); :: thesis: ( k < card Affn & B = { pnA where pnA is Element of (() | (Affin Affn)) : (pnA |-- E) | k in Ak } implies ( Ak is closed iff B is closed ) )
assume that
A1: k < card Affn and
A2: B = { v where v is Element of (() | (Affin Affn)) : (v |-- E) | k in Ak } ; :: thesis: ( Ak is closed iff B is closed )
set B1 = { v where v is Element of (() | (Affin Affn)) : (v |-- E) | k in Ak ` } ;
A3: B ` c= { v where v is Element of (() | (Affin Affn)) : (v |-- E) | k in Ak ` }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B ` or x in { v where v is Element of (() | (Affin Affn)) : (v |-- E) | k in Ak ` } )
assume A4: x in B ` ; :: thesis: x in { v where v is Element of (() | (Affin Affn)) : (v |-- E) | k in Ak ` }
then reconsider v = x as Element of (() | (Affin Affn)) ;
set vE = v |-- E;
len (v |-- E) = card Affn by Th16;
then len ((v |-- E) | k) = k by ;
then A5: (v |-- E) | k in [#] () by TOPREAL3:46;
not v in B by ;
then not (v |-- E) | k in Ak by A2;
then (v |-- E) | k in Ak ` by ;
hence x in { v where v is Element of (() | (Affin Affn)) : (v |-- E) | k in Ak ` } ; :: thesis: verum
end;
A6: not Affn is empty by A1;
{ v where v is Element of (() | (Affin Affn)) : (v |-- E) | k in Ak ` } c= B `
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of (() | (Affin Affn)) : (v |-- E) | k in Ak ` } or x in B ` )
assume x in { v where v is Element of (() | (Affin Affn)) : (v |-- E) | k in Ak ` } ; :: thesis: x in B `
then consider v being Element of (() | (Affin Affn)) such that
A7: x = v and
A8: (v |-- E) | k in Ak ` ;
assume not x in B ` ; :: thesis: contradiction
then v in B by ;
then ex w being Element of (() | (Affin Affn)) st
( w = v & (w |-- E) | k in Ak ) by A2;
hence contradiction by A8, XBOOLE_0:def 5; :: thesis: verum
set vE = v |-- E;
end;
then { v where v is Element of (() | (Affin Affn)) : (v |-- E) | k in Ak ` } = B ` by A3;
then ( Ak ` is open iff B ` is open ) by ;
hence ( Ak is closed iff B is closed ) by TOPS_1:3; :: thesis: verum