set TRn = TOP-REAL n;

let A be Subset of (TOP-REAL n); :: thesis: ( A is Affine implies A is closed )

assume A is Affine ; :: thesis: A is closed

then A1: Affin A = A by RLAFFIN1:50;

let A be Subset of (TOP-REAL n); :: thesis: ( A is Affine implies A is closed )

assume A is Affine ; :: thesis: A is closed

then A1: Affin A = A by RLAFFIN1:50;

per cases
( A is empty or not A is empty )
;

end;

suppose A2:
not A is empty
; :: thesis: 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 }

{ v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P } c= Affin A

hence A is closed by A1, A9, A22, A13, Th26; :: thesis: verum

end;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 }

proof

A22:
card IB <= n
by A10, NAT_1:13;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Affin A or x in { v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P } )

assume A20: x in Affin A ; :: thesis: x in { v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P }

then reconsider v = x as Element of (TOP-REAL n) ;

set vP = v |-- P12;

A21: v |-- P12 = ((v |-- P12) | (card IB)) ^ ((v |-- P12) /^ (card IB)) by RFINSEQ:8;

v |-- P12 = ((card IB) |-> 0) ^ ((v |-- P12) /^ (card IB)) by A1, A3, A5, A8, A18, A17, A11, A20, Th22;

then (v |-- P12) | (card IB) = (card IB) |-> 0 by A21, FINSEQ_1:33;

then (v |-- P12) | (card IB) in P by TARSKI:def 1;

hence x in { v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P } ; :: thesis: verum

end;assume A20: x in Affin A ; :: thesis: x in { v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P }

then reconsider v = x as Element of (TOP-REAL n) ;

set vP = v |-- P12;

A21: v |-- P12 = ((v |-- P12) | (card IB)) ^ ((v |-- P12) /^ (card IB)) by RFINSEQ:8;

v |-- P12 = ((card IB) |-> 0) ^ ((v |-- P12) /^ (card IB)) by A1, A3, A5, A8, A18, A17, A11, A20, Th22;

then (v |-- P12) | (card IB) = (card IB) |-> 0 by A21, FINSEQ_1:33;

then (v |-- P12) | (card IB) in P by TARSKI:def 1;

hence x in { v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P } ; :: thesis: verum

{ v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P } c= Affin A

proof

then
{ v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P } = Affin A
by A19;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P } or x in Affin A )

assume x in { v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P } ; :: thesis: x in Affin A

then consider v being Element of (TOP-REAL n) such that

A23: x = v and

A24: (v |-- P12) | (card IB) in P ;

set vP = v |-- P12;

(v |-- P12) | (card IB) = (card IB) |-> 0 by A24, TARSKI:def 1;

then v |-- P12 = ((card IB) |-> 0) ^ ((v |-- P12) /^ (card IB)) by RFINSEQ:8;

hence x in Affin A by A1, A3, A5, A8, A18, A17, A11, A23, Th22; :: thesis: verum

end;assume x in { v where v is Element of (TOP-REAL n) : (v |-- P12) | (card IB) in P } ; :: thesis: x in Affin A

then consider v being Element of (TOP-REAL n) such that

A23: x = v and

A24: (v |-- P12) | (card IB) in P ;

set vP = v |-- P12;

(v |-- P12) | (card IB) = (card IB) |-> 0 by A24, TARSKI:def 1;

then v |-- P12 = ((card IB) |-> 0) ^ ((v |-- P12) /^ (card IB)) by RFINSEQ:8;

hence x in Affin A by A1, A3, A5, A8, A18, A17, A11, A23, Th22; :: thesis: verum

hence A is closed by A1, A9, A22, A13, Th26; :: thesis: verum