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

let An be Subset of (); :: thesis: for Affn being affinely-independent Subset of ()
for Ak being Subset of ()
for EN being Enumeration of Affn st k <= n & card Affn = n + 1 & An = { pn where pn is Point of () : (pn |-- EN) | k in Ak } holds
( Ak is closed iff An is closed )

let Affn be affinely-independent Subset of (); :: thesis: for Ak being Subset of ()
for EN being Enumeration of Affn st k <= n & card Affn = n + 1 & An = { pn where pn is Point of () : (pn |-- EN) | k in Ak } holds
( Ak is closed iff An is closed )

let Ak be Subset of (); :: thesis: for EN being Enumeration of Affn st k <= n & card Affn = n + 1 & An = { pn where pn is Point of () : (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 () : (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 () : (v |-- E) | k in Ak } ; :: thesis: ( Ak is closed iff An is closed )
set B1 = { v where v is Element of () : (v |-- E) | k in Ak ` } ;
A3: k < card Affn by ;
A4: An ` c= { v where v is Element of () : (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 () : (v |-- E) | k in Ak ` } )
assume A5: x in An ` ; :: thesis: x in { v where v is Element of () : (v |-- E) | k in Ak ` }
then reconsider f = x as Element of () ;
set fE = f |-- E;
len (f |-- E) = card Affn by Th16;
then len ((f |-- E) | k) = k by ;
then A6: (f |-- E) | k is Element of () by TOPREAL3:46;
assume not x in { v where v is Element of () : (v |-- E) | k in Ak ` } ; :: thesis: contradiction
then not (f |-- E) | k in Ak ` ;
then (f |-- E) | k in Ak by ;
then f in An by A2;
hence contradiction by A5, XBOOLE_0:def 5; :: thesis: verum
end;
{ v where v is Element of () : (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 () : (v |-- E) | k in Ak ` } or x in An ` )
assume x in { v where v is Element of () : (v |-- E) | k in Ak ` } ; :: thesis: x in An `
then consider v being Element of () such that
A7: x = v and
A8: (v |-- E) | k in Ak ` ;
assume not x in An ` ; :: thesis: contradiction
then v in An by ;
then ex w being Element of () 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 () : (v |-- E) | k in Ak ` } by A4;
then ( Ak ` is open iff An ` is open ) by ;
hence ( Ak is closed iff An is closed ) by TOPS_1:3; :: thesis: verum