let n, k be Nat; :: thesis: for Affn being affinely-independent Subset of (TOP-REAL n)
for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn
for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds
( Ak is closed iff B is closed )
let Affn be affinely-independent Subset of (TOP-REAL n); :: thesis: for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn
for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds
( Ak is closed iff B is closed )
let Ak be Subset of (TOP-REAL k); :: thesis: for EN being Enumeration of Affn
for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (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 ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (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 ((TOP-REAL n) | (Affin Affn)); :: thesis: ( k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (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 ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak } ; :: thesis: ( Ak is closed iff B is closed )
set B1 = { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak ` } ;
A3: B ` c= { v where v is Element of ((TOP-REAL n) | (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 ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak ` } )
assume A4: x in B ` ; :: thesis: x in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak ` }
then reconsider v = x as Element of ((TOP-REAL n) | (Affin Affn)) ;
set vE = v |-- E;
len (v |-- E) = card Affn by Th16;
then len ((v |-- E) | k) = k by A1, FINSEQ_1:59;
then A5: (v |-- E) | k in [#] (TOP-REAL k) by TOPREAL3:46;
not v in B by A4, XBOOLE_0:def 5;
then not (v |-- E) | k in Ak by A2;
then (v |-- E) | k in Ak ` by A5, XBOOLE_0:def 5;
hence x in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak ` } ; :: thesis: verum

end;

A6: not Affn is empty by A1;
{ v where v is Element of ((TOP-REAL n) | (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 ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak ` } or x in B ` )
assume x in { v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak ` } ; :: thesis: x in B `
then consider v being Element of ((TOP-REAL n) | (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 A6, A7, XBOOLE_0:def 5;
then ex w being Element of ((TOP-REAL n) | (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 ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak ` } = B ` by A3;
then ( Ak ` is open iff B ` is open ) by A1, Th27;
hence ( Ak is closed iff B is closed ) by TOPS_1:3; :: thesis: verum