set TRn = TOP-REAL n;
let A be Subset of (); :: 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 ) ;
suppose A is empty ; :: thesis: A is closed
end;
suppose A2: not A is empty ; :: thesis: A is closed
{} () c= A ;
then consider Ia being affinely-independent Subset of () such that
{} c= Ia and
Ia c= A and
A3: Affin Ia = A by ;
consider IA being affinely-independent Subset of () such that
A4: Ia c= IA and
IA c= [#] () and
A5: Affin IA = Affin ([#] ()) by RLAFFIN1:60;
reconsider IB = IA \ Ia as affinely-independent Subset of () by ;
set cIB = card IB;
A6: dim () = n by Th4;
then A7: card IB <= n + 1 by Th5;
[#] () is Affine by RUSUB_4:22;
then A8: Affin ([#] ()) = [#] () 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 ;
then IA <> IB by XBOOLE_1:83;
then card IB <> n + 1 by ;
then A10: card IB < n + 1 by ;
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 ;
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 ;
Ia \/ IB = Ia \/ IA by XBOOLE_1:39
.= IA by ;
then rng ( the Enumeration of IB ^ the Enumeration of Ia) = IA by ;
then reconsider P12 = the Enumeration of IB ^ the Enumeration of Ia as Enumeration of IA by ;
len the Enumeration of IB = card IB by ;
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 () : (v |-- P12) | (card IB) in P } ;
A18: IA \ IB = IA /\ Ia by XBOOLE_1:48
.= Ia by ;
A19: Affin A c= { v where v is Element of () : (v |-- P12) | (card IB) in P }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Affin A or x in { v where v is Element of () : (v |-- P12) | (card IB) in P } )
assume A20: x in Affin A ; :: thesis: x in { v where v is Element of () : (v |-- P12) | (card IB) in P }
then reconsider v = x as Element of () ;
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 ;
then (v |-- P12) | (card IB) in P by TARSKI:def 1;
hence x in { v where v is Element of () : (v |-- P12) | (card IB) in P } ; :: thesis: verum
end;
A22: card IB <= n by ;
{ v where v is Element of () : (v |-- P12) | (card IB) in P } c= Affin A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of () : (v |-- P12) | (card IB) in P } or x in Affin A )
assume x in { v where v is Element of () : (v |-- P12) | (card IB) in P } ; :: thesis: x in Affin A
then consider v being Element of () 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 ;
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;
then { v where v is Element of () : (v |-- P12) | (card IB) in P } = Affin A by A19;
hence A is closed by A1, A9, A22, A13, Th26; :: thesis: verum
end;
end;