set TRn = TOP-REAL n;
let A be Subset of (TOP-REAL n); ( A is Affine implies A is closed )
assume
A is Affine
; A is closed
then A1:
Affin A = A
by RLAFFIN1:50;
per cases
( A is empty or not A is empty )
;
suppose A2:
not
A is
empty
;
A is closed
{} (TOP-REAL n) c= A
;
then consider Ia being
affinely-independent Subset of
(TOP-REAL n) such that
{} c= Ia
and
Ia c= A
and A3:
Affin Ia = A
by A1, RLAFFIN1:60;
consider IA being
affinely-independent Subset of
(TOP-REAL n) such that A4:
Ia c= IA
and
IA c= [#] (TOP-REAL n)
and A5:
Affin IA = Affin ([#] (TOP-REAL n))
by RLAFFIN1:60;
reconsider IB =
IA \ Ia as
affinely-independent Subset of
(TOP-REAL n) by RLAFFIN1:43, XBOOLE_1:36;
set cIB =
card IB;
A6:
dim (TOP-REAL n) = n
by Th4;
then A7:
card IB <= n + 1
by Th5;
[#] (TOP-REAL n) is
Affine
by RUSUB_4:22;
then A8:
Affin ([#] (TOP-REAL n)) = [#] (TOP-REAL n)
by RLAFFIN1:50;
then A9:
card IA = n + 1
by A5, A6, Th6;
not
Ia is
empty
by A2, A3;
then
IA meets Ia
by A4, XBOOLE_1:67;
then
IA <> IB
by XBOOLE_1:83;
then
card IB <> n + 1
by A9, CARD_2:102, XBOOLE_1:36;
then A10:
card IB < n + 1
by A7, XXREAL_0:1;
then A11:
card IB < card IA
by A5, A8, A6, Th6;
set TRc =
TOP-REAL (card IB);
A12:
0* (card IB) = 0. (TOP-REAL (card IB))
by EUCLID:66;
then
(card IB) |-> 0 is
Element of
(TOP-REAL (card IB))
by EUCLID:def 4;
then reconsider P =
{((card IB) |-> 0)} as
Subset of
(TOP-REAL (card IB)) by ZFMISC_1:31;
0* (card IB) = (card IB) |-> 0
by EUCLID:def 4;
then A13:
P is
closed
by A12, PCOMPS_1:7;
set P1 = the
Enumeration of
Ia;
A14:
rng the
Enumeration of
Ia = Ia
by Def1;
set P2 = the
Enumeration of
IB;
set P12 = the
Enumeration of
IB ^ the
Enumeration of
Ia;
A15:
rng the
Enumeration of
IB = IB
by Def1;
Ia misses IB
by XBOOLE_1:79;
then A16:
the
Enumeration of
IB ^ the
Enumeration of
Ia is
one-to-one
by A14, A15, FINSEQ_3:91;
Ia \/ IB =
Ia \/ IA
by XBOOLE_1:39
.=
IA
by A4, XBOOLE_1:12
;
then
rng ( the Enumeration of IB ^ the Enumeration of Ia) = IA
by A14, A15, FINSEQ_1:31;
then reconsider P12 = the
Enumeration of
IB ^ the
Enumeration of
Ia as
Enumeration of
IA by A16, Def1;
len the
Enumeration of
IB = card IB
by A15, FINSEQ_4:62;
then A17:
P12 .: (Seg (card IB)) =
P12 .: (dom the Enumeration of IB)
by FINSEQ_1:def 3
.=
rng (P12 | (dom the Enumeration of IB))
by RELAT_1:115
.=
rng the
Enumeration of
IB
by FINSEQ_1:21
.=
IB
by Def1
;
set B =
{ v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P } ;
A18:
IA \ IB =
IA /\ Ia
by XBOOLE_1:48
.=
Ia
by A4, XBOOLE_1:28
;
A19:
Affin A c= { v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P }
A22:
card IB <= n
by A10, NAT_1:13;
{ v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P } c= Affin A
then
{ v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P } = Affin A
by A19;
hence
A is
closed
by A1, A9, A22, A13, Th26;
verum end;