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

{ v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak ` } c= B `

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

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

A6:
not Affn is empty
by A1;
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;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

{ v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak ` } c= B `

proof

then
{ v where v is Element of ((TOP-REAL n) | (Affin Affn)) : (v |-- E) | k in Ak ` } = B `
by A3;
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;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;

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