let n, k be Nat; :: thesis: for An being Subset of (TOP-REAL n)
for Affn being affinely-independent Subset of (TOP-REAL n)
for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds
( Ak is closed iff An is closed )
let An be Subset of (TOP-REAL n); :: 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 st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds
( Ak is closed iff An 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 st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds
( Ak is closed iff An is closed )
let Ak be Subset of (TOP-REAL k); :: thesis: for EN being Enumeration of Affn st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds
( Ak is closed iff An is closed )
set TRn = TOP-REAL n;
set TRk = TOP-REAL k;
set A = Affn;
let E be Enumeration of Affn; :: thesis: ( k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- E) | k in Ak } implies ( Ak is closed iff An is closed ) )
assume that
A1: ( k <= n & card Affn = n + 1 ) and
A2: An = { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak } ; :: thesis: ( Ak is closed iff An is closed )
set B1 = { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } ;
A3: k < card Affn by A1, NAT_1:13;
A4: An ` c= { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in An ` or x in { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } )
assume A5: x in An ` ; :: thesis: x in { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` }
then reconsider f = x as Element of (TOP-REAL n) ;
set fE = f |-- E;
len (f |-- E) = card Affn by Th16;
then len ((f |-- E) | k) = k by A3, FINSEQ_1:59;
then A6: (f |-- E) | k is Element of (TOP-REAL k) by TOPREAL3:46;
assume not x in { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } ; :: thesis: contradiction
then not (f |-- E) | k in Ak ` ;
then (f |-- E) | k in Ak by A6, XBOOLE_0:def 5;
then f in An by A2;
hence contradiction by A5, XBOOLE_0:def 5; :: thesis: verum

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } or x in An ` )
assume x in { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } ; :: thesis: x in An `
then consider v being Element of (TOP-REAL n) such that
A7: x = v and
A8: (v |-- E) | k in Ak ` ;
assume not x in An ` ; :: thesis: contradiction
then v in An by A7, XBOOLE_0:def 5;
then ex w being Element of (TOP-REAL n) st
( v = w & (w |-- E) | k in Ak ) by A2;
hence contradiction by A8, XBOOLE_0:def 5; :: thesis: verum

end;

then An ` = { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } by A4;
then ( Ak ` is open iff An ` is open ) by A1, Th25;
hence ( Ak is closed iff An is closed ) by TOPS_1:3; :: thesis: verum