let n be Nat; :: thesis: for A being affinely-independent Subset of (TOP-REAL n) 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 (TOP-REAL n); :: 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 H₁( object ) -> Element of bool the carrier of (TOP-REAL n) = (|-- (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 = H₁(k) from FINSEQ_1:sch 2();
A4: dom f = Seg (len f) by FINSEQ_1:def 3;
then A5: not rng f is empty by A2, RELAT_1:42;
rng f c= bool the carrier of (TOP-REAL n)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in bool the carrier of (TOP-REAL n) )
assume y in rng f ; :: thesis: y in bool the carrier of (TOP-REAL n)
then consider x being object such that
A6: x in dom f and
A7: f . x = y by FUNCT_1:def 3;
f . x = H₁(x) by A3, A6;
hence y in bool the carrier of (TOP-REAL n) by A7; :: thesis: verum

end;

then reconsider f = f as FinSequence of bool the carrier of (TOP-REAL n) 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 (TOP-REAL n) st v in A holds
(x |-- A) . v >= 0

let v be Element of (TOP-REAL n); :: 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 A8, FUNCT_1:def 3;
A15: k in dom f by A1, A2, A9, A4, A13, FINSEQ_1:def 3;
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 A11, Def3;
f . k = (|-- (A,v)) " L by A3, A14, A15;
then (x |-- A) . v in L by A11, A17, A16, FUNCT_1:def 7;
hence (x |-- A) . v >= 0 by XXREAL_1:1; :: thesis: verum

end;

dim (TOP-REAL n) = n by Th4;
then [#] (TOP-REAL n) = Affin A by A1, Th6;
hence x in conv A by A11, A12, RLAFFIN1:73; :: 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 A1, A2, A8, A9, A4, A18, A21, FUNCT_1:def 3;
then reconsider Ek = the Enumeration of A . k as Element of (TOP-REAL n) ;
A23: dom (|-- (A,Ek)) = [#] (TOP-REAL n) by FUNCT_2:def 1;
A24: ( 0 <= (x |-- A) . Ek & (x |-- A) . Ek <= 1 ) by A20, RLAFFIN1:71;
(x |-- A) . Ek = (|-- (A,Ek)) . x by A20, Def3;
then A25: (|-- (A,Ek)) . x in L by A24, XXREAL_1:1;
Y = (|-- (A,( the Enumeration of A . k))) " L by A3, A21, A22;
hence x in Y by A20, A25, A23, FUNCT_1:def 7; :: thesis: verum

end;

hence x in meet (rng f) by A5, SETFAM_1:def 1; :: thesis: verum

end;

now :: thesis: for B being Subset of (TOP-REAL n) st B in rng f holds
B is closed

let B be Subset of (TOP-REAL n); :: 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 A1, Th32, TREAL_1:1;
then (|-- (A,( the Enumeration of A . k))) " L is closed by PRE_TOPC:def 6;
hence B is closed by A3, A26; :: 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 A19, A10, XBOOLE_0:def 10; :: thesis: verum