let n be Nat; :: thesis: for A being affinely-independent Subset of () st card A = n + 1 holds
conv A is closed

set L = [.0,1.];
set TRn = TOP-REAL n;
let A be affinely-independent Subset of (); :: thesis: ( card A = n + 1 implies conv A is closed )
assume A1: card A = n + 1 ; :: thesis: conv A is closed
reconsider L = [.0,1.] as Subset of R^1 by TOPMETR:17;
set E = the Enumeration of A;
deffunc H1( object ) -> Element of bool the carrier of () = (|-- (A,( the Enumeration of A . \$1))) " L;
consider f being FinSequence such that
A2: len f = n + 1 and
A3: for k being Nat st k in dom f holds
f . k = H1(k) from A4: dom f = Seg (len f) by FINSEQ_1:def 3;
then A5: not rng f is empty by ;
rng f c= bool the carrier of ()
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in bool the carrier of () )
assume y in rng f ; :: thesis: y in bool the carrier of ()
then consider x being object such that
A6: x in dom f and
A7: f . x = y by FUNCT_1:def 3;
f . x = H1(x) by A3, A6;
hence y in bool the carrier of () by A7; :: thesis: verum
end;
then reconsider f = f as FinSequence of bool the carrier of () by FINSEQ_1:def 4;
A8: rng the Enumeration of A = A by Def1;
then A9: len the Enumeration of A = card A by FINSEQ_4:62;
A10: meet (rng f) c= conv A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet (rng f) or x in conv A )
assume A11: x in meet (rng f) ; :: thesis: x in conv A
A12: now :: thesis: for v being Element of () st v in A holds
(x |-- A) . v >= 0
let v be Element of (); :: thesis: ( v in A implies (x |-- A) . v >= 0 )
assume v in A ; :: thesis: (x |-- A) . v >= 0
then consider k being object such that
A13: k in dom the Enumeration of A and
A14: the Enumeration of A . k = v by ;
A15: k in dom f by ;
then f . k in rng f by FUNCT_1:def 3;
then A16: meet (rng f) c= f . k by SETFAM_1:3;
A17: (x |-- A) . v = (|-- (A,v)) . x by ;
f . k = (|-- (A,v)) " L by A3, A14, A15;
then (x |-- A) . v in L by ;
hence (x |-- A) . v >= 0 by XXREAL_1:1; :: thesis: verum
end;
dim () = n by Th4;
then [#] () = Affin A by ;
hence x in conv A by ; :: thesis: verum
end;
A18: dom the Enumeration of A = Seg (len the Enumeration of A) by FINSEQ_1:def 3;
A19: conv A c= meet (rng f)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in conv A or x in meet (rng f) )
assume A20: x in conv A ; :: thesis: x in meet (rng f)
now :: thesis: for Y being set st Y in rng f holds
x in Y
let Y be set ; :: thesis: ( Y in rng f implies x in Y )
assume Y in rng f ; :: thesis: x in Y
then consider k being object such that
A21: k in dom f and
A22: f . k = Y by FUNCT_1:def 3;
the Enumeration of A . k in A by ;
then reconsider Ek = the Enumeration of A . k as Element of () ;
A23: dom (|-- (A,Ek)) = [#] () by FUNCT_2:def 1;
A24: ( 0 <= (x |-- A) . Ek & (x |-- A) . Ek <= 1 ) by ;
(x |-- A) . Ek = (|-- (A,Ek)) . x by ;
then A25: (|-- (A,Ek)) . x in L by ;
Y = (|-- (A,( the Enumeration of A . k))) " L by A3, A21, A22;
hence x in Y by ; :: thesis: verum
end;
hence x in meet (rng f) by ; :: thesis: verum
end;
now :: thesis: for B being Subset of () st B in rng f holds
B is closed
let B be Subset of (); :: thesis: ( B in rng f implies B is closed )
assume B in rng f ; :: thesis: B is closed
then consider k being object such that
A26: ( k in dom f & f . k = B ) by FUNCT_1:def 3;
( |-- (A,( the Enumeration of A . k)) is continuous & L is closed ) by ;
then (|-- (A,( the Enumeration of A . k))) " L is closed by PRE_TOPC:def 6;
hence B is closed by ; :: thesis: verum
end;
then rng f is closed by TOPS_2:def 2;
then meet (rng f) is closed by TOPS_2:22;
hence conv A is closed by ; :: thesis: verum