let n, k be Nat; :: thesis: for Affn being affinely-independent Subset of ()
for Ak being Subset of ()
for EN being Enumeration of Affn
for An being Subset of () st k <= n & card Affn = n + 1 & An = { pn where pn is Point of () : (pn |-- EN) | k in Ak } holds
( Ak is open iff An is open )

let Affn be affinely-independent Subset of (); :: thesis: for Ak being Subset of ()
for EN being Enumeration of Affn
for An being Subset of () st k <= n & card Affn = n + 1 & An = { pn where pn is Point of () : (pn |-- EN) | k in Ak } holds
( Ak is open iff An is open )

let Ak be Subset of (); :: thesis: for EN being Enumeration of Affn
for An being Subset of () st k <= n & card Affn = n + 1 & An = { pn where pn is Point of () : (pn |-- EN) | k in Ak } holds
( Ak is open iff An is open )

set A = Affn;
set AA = Affin Affn;
set TRn = TOP-REAL n;
let EN be Enumeration of Affn; :: thesis: for An being Subset of () st k <= n & card Affn = n + 1 & An = { pn where pn is Point of () : (pn |-- EN) | k in Ak } holds
( Ak is open iff An is open )

let An be Subset of (); :: thesis: ( k <= n & card Affn = n + 1 & An = { pn where pn is Point of () : (pn |-- EN) | k in Ak } implies ( Ak is open iff An is open ) )
assume that
A1: k <= n and
A2: card Affn = n + 1 and
A3: An = { v where v is Element of () : (v |-- EN) | k in Ak } ; :: thesis: ( Ak is open iff An is open )
set E = EN;
A4: rng EN = Affn by Def1;
then A5: len EN = card Affn by FINSEQ_4:62;
then A6: len EN >= 1 by ;
then A7: len EN in dom EN by FINSEQ_3:25;
then EN . (len EN) in Affn by ;
then reconsider EL = EN . (len EN) as Element of () ;
A8: card ((- EL) + Affn) = n + 1 by ;
set BB = { u where u is Element of () : ( u in Affin Affn & (u |-- EN) | k in Ak ) } ;
A9: { u where u is Element of () : ( u in Affin Affn & (u |-- EN) | k in Ak ) } c= An
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { u where u is Element of () : ( u in Affin Affn & (u |-- EN) | k in Ak ) } or x in An )
assume x in { u where u is Element of () : ( u in Affin Affn & (u |-- EN) | k in Ak ) } ; :: thesis: x in An
then ex u being Element of () st
( x = u & u in Affin Affn & (u |-- EN) | k in Ak ) ;
hence x in An by A3; :: thesis: verum
end;
reconsider Ev = EN + ((card Affn) |-> (- EL)) as Enumeration of (- EL) + Affn by Th13;
set TB = { w where w is Element of () : (w |-- Ev) | k in Ak } ;
set T = transl ((- EL),());
A10: dim () = n by Th4;
then A11: [#] () = Affin Affn by ;
An c= { u where u is Element of () : ( u in Affin Affn & (u |-- EN) | k in Ak ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in An or x in { u where u is Element of () : ( u in Affin Affn & (u |-- EN) | k in Ak ) } )
assume x in An ; :: thesis: x in { u where u is Element of () : ( u in Affin Affn & (u |-- EN) | k in Ak ) }
then consider v being Element of () such that
A12: ( x = v & (v |-- EN) | k in Ak ) by A3;
thus x in { u where u is Element of () : ( u in Affin Affn & (u |-- EN) | k in Ak ) } by ; :: thesis: verum
end;
then { u where u is Element of () : ( u in Affin Affn & (u |-- EN) | k in Ak ) } = An by A9;
then A13: (transl ((- EL),())) .: An = { w where w is Element of () : ( w in Affin ((- EL) + Affn) & (w |-- Ev) | k in Ak ) } by Lm6;
A14: (transl ((- EL),())) .: An c= { w where w is Element of () : (w |-- Ev) | k in Ak }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (transl ((- EL),())) .: An or x in { w where w is Element of () : (w |-- Ev) | k in Ak } )
assume x in (transl ((- EL),())) .: An ; :: thesis: x in { w where w is Element of () : (w |-- Ev) | k in Ak }
then ex w being Element of () st
( x = w & w in Affin ((- EL) + Affn) & (w |-- Ev) | k in Ak ) by A13;
hence x in { w where w is Element of () : (w |-- Ev) | k in Ak } ; :: thesis: verum
end;
A15: card ((- EL) + Affn) = card Affn by RLAFFIN1:7;
then A16: Affin ((- EL) + Affn) = [#] () by A2, A10, Th6;
{ w where w is Element of () : (w |-- Ev) | k in Ak } c= (transl ((- EL),())) .: An
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of () : (w |-- Ev) | k in Ak } or x in (transl ((- EL),())) .: An )
assume x in { w where w is Element of () : (w |-- Ev) | k in Ak } ; :: thesis: x in (transl ((- EL),())) .: An
then consider w being Element of () such that
A17: ( x = w & (w |-- Ev) | k in Ak ) ;
thus x in (transl ((- EL),())) .: An by ; :: thesis: verum
end;
then A18: (transl ((- EL),())) .: An = { w where w is Element of () : (w |-- Ev) | k in Ak } by A14;
len EN in Seg (card Affn) by A5, A6;
then A19: ((card Affn) |-> (- EL)) . (len EN) = - EL by FINSEQ_2:57;
A20: rng Ev = (- EL) + Affn by Def1;
then len Ev = card Affn by ;
then dom EN = dom Ev by ;
then Ev . (len EN) = EL + (- EL) by
.= 0. () by RLVECT_1:5
.= 0* n by EUCLID:70 ;
then A21: Ev . (len Ev) = 0* n by ;
not (- EL) + Affn is empty by ;
then ( (transl ((- EL),())) .: An is open iff Ak is open ) by A1, A21, A8, A18, Lm7;
hence ( Ak is open iff An is open ) by TOPGRP_1:25; :: thesis: verum
set TAA = (transl ((- EL),())) .: (Affin Affn);
A22: rng ((transl ((- EL),())) | (Affin Affn)) = (transl ((- EL),())) .: (Affin Affn) by RELAT_1:115;
dom (transl ((- EL),())) = [#] () by FUNCT_2:52;
then A23: dom ((transl ((- EL),())) | (Affin Affn)) = Affin Affn by RELAT_1:62;
( [#] (() | (Affin Affn)) = Affin Affn & [#] (() | ((transl ((- EL),())) .: (Affin Affn))) = (transl ((- EL),())) .: (Affin Affn) ) by PRE_TOPC:def 5;
then reconsider TA = (transl ((- EL),())) | (Affin Affn) as Function of (() | (Affin Affn)),(() | ((transl ((- EL),())) .: (Affin Affn))) by ;
reconsider TAB = TA .: An as Subset of (() | ((transl ((- EL),())) .: (Affin Affn))) ;
reconsider TAB = TA .: An as Subset of (() | ((transl ((- EL),())) .: (Affin Affn))) ;