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 B being Subset of (() | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of (() | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds
( Ak is open iff B is open )

let Affn be affinely-independent Subset of (); :: thesis: for Ak being Subset of ()
for EN being Enumeration of Affn
for B being Subset of (() | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of (() | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds
( Ak is open iff B is open )

let Ak be Subset of (); :: thesis: for EN being Enumeration of Affn
for B being Subset of (() | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of (() | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds
( Ak is open iff B is open )

let EN be Enumeration of Affn; :: thesis: for B being Subset of (() | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of (() | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds
( Ak is open iff B is open )

set E = EN;
set Tn = TOP-REAL n;
set Tk = TOP-REAL k;
set A = Affn;
set cA = (card Affn) -' 1;
set TcA = TOP-REAL ((card Affn) -' 1);
set AA = Affin Affn;
let B be Subset of (() | (Affin Affn)); :: thesis: ( k < card Affn & B = { pnA where pnA is Element of (() | (Affin Affn)) : (pnA |-- EN) | k in Ak } implies ( Ak is open iff B is open ) )
assume that
A1: k < card Affn and
A2: B = { v where v is Element of (() | (Affin Affn)) : (v |-- EN) | k in Ak } ; :: thesis: ( Ak is open iff B is open )
set BB = { u where u is Element of () : ( u in Affin Affn & (u |-- EN) | k in Ak ) } ;
A3: [#] (() | (Affin Affn)) = Affin Affn by PRE_TOPC:def 5;
A4: { u where u is Element of () : ( u in Affin Affn & (u |-- EN) | k in Ak ) } c= B
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 B )
assume x in { u where u is Element of () : ( u in Affin Affn & (u |-- EN) | k in Ak ) } ; :: thesis: x in B
then consider u being Element of () such that
A5: ( x = u & u in Affin Affn & (u |-- EN) | k in Ak ) ;
thus x in B by A2, A3, A5; :: thesis: verum
end;
A6: not Affn is empty by A1;
B 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 B or x in { u where u is Element of () : ( u in Affin Affn & (u |-- EN) | k in Ak ) } )
assume x in B ; :: thesis: x in { u where u is Element of () : ( u in Affin Affn & (u |-- EN) | k in Ak ) }
then consider u being Element of (() | (Affin Affn)) such that
A7: ( x = u & (u |-- EN) | k in Ak ) by A2;
not Affin Affn is empty by A6;
then u in Affin Affn by A3;
hence x in { u where u is Element of () : ( u in Affin Affn & (u |-- EN) | k in Ak ) } by A7; :: thesis: verum
end;
then A8: { u where u is Element of () : ( u in Affin Affn & (u |-- EN) | k in Ak ) } = B by A4;
A9: rng EN = Affn by Def1;
then A10: len EN = card Affn by FINSEQ_4:62;
then A11: len EN >= 1 by ;
then A12: 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 () ;
len EN in Seg (card Affn) by ;
then A13: ((card Affn) |-> (- EL)) . (len EN) = - EL by FINSEQ_2:57;
A14: k < card ((- EL) + Affn) by ;
set T = transl ((- EL),());
set TAA = (transl ((- EL),())) .: (Affin Affn);
A15: [#] (() | ((transl ((- EL),())) .: (Affin Affn))) = (transl ((- EL),())) .: (Affin Affn) by PRE_TOPC:def 5;
A16: rng ((transl ((- EL),())) | (Affin Affn)) = (transl ((- EL),())) .: (Affin Affn) by RELAT_1:115;
A17: dom (transl ((- EL),())) = [#] () by FUNCT_2:52;
then dom ((transl ((- EL),())) | (Affin Affn)) = Affin Affn by RELAT_1:62;
then reconsider TA = (transl ((- EL),())) | (Affin Affn) as Function of (() | (Affin Affn)),(() | ((transl ((- EL),())) .: (Affin Affn))) by ;
reconsider TAB = TA .: B as Subset of (() | ((transl ((- EL),())) .: (Affin Affn))) ;
A18: TA is being_homeomorphism by METRIZTS:2;
reconsider Ev = EN + ((card Affn) |-> (- EL)) as Enumeration of (- EL) + Affn by Th13;
A19: card ((- EL) + Affn) = card Affn by RLAFFIN1:7;
then A20: not (- EL) + Affn is empty by A1;
A21: 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 A22: Ev . (len Ev) = 0* n by ;
set Tab = { w where w is Element of (() | ((transl ((- EL),())) .: (Affin Affn))) : (w |-- Ev) | k in Ak } ;
A23: (- EL) + (Affin Affn) = Affin ((- EL) + Affn) by RLAFFIN1:53;
then A24: (transl ((- EL),())) .: (Affin Affn) = Affin ((- EL) + Affn) by RLTOPSP1:33;
TA .: B = (transl ((- EL),())) .: B by ;
then A25: TAB = { w where w is Element of () : ( w in Affin ((- EL) + Affn) & (w |-- Ev) | k in Ak ) } by ;
A26: TAB c= { w where w is Element of (() | ((transl ((- EL),())) .: (Affin Affn))) : (w |-- Ev) | k in Ak }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in TAB or x in { w where w is Element of (() | ((transl ((- EL),())) .: (Affin Affn))) : (w |-- Ev) | k in Ak } )
assume x in TAB ; :: thesis: x in { w where w is Element of (() | ((transl ((- EL),())) .: (Affin Affn))) : (w |-- Ev) | k in Ak }
then consider w being Element of () such that
A27: x = w and
A28: w in Affin ((- EL) + Affn) and
A29: (w |-- Ev) | k in Ak by A25;
w in (transl ((- EL),())) .: (Affin Affn) by ;
hence x in { w where w is Element of (() | ((transl ((- EL),())) .: (Affin Affn))) : (w |-- Ev) | k in Ak } by ; :: thesis: verum
end;
A30: not (transl ((- EL),())) .: (Affin Affn) is empty by ;
{ w where w is Element of (() | ((transl ((- EL),())) .: (Affin Affn))) : (w |-- Ev) | k in Ak } c= TAB
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of (() | ((transl ((- EL),())) .: (Affin Affn))) : (w |-- Ev) | k in Ak } or x in TAB )
assume x in { w where w is Element of (() | ((transl ((- EL),())) .: (Affin Affn))) : (w |-- Ev) | k in Ak } ; :: thesis: x in TAB
then consider w being Element of (() | ((transl ((- EL),())) .: (Affin Affn))) such that
A31: ( x = w & (w |-- Ev) | k in Ak ) ;
w in (transl ((- EL),())) .: (Affin Affn) by ;
hence x in TAB by ; :: thesis: verum
end;
then TAB = { w where w is Element of (() | ((transl ((- EL),())) .: (Affin Affn))) : (w |-- Ev) | k in Ak } by A26;
then ( TAB is open iff Ak is open ) by A24, A22, A14, A20, Lm8;
hence ( Ak is open iff B is open ) by ; :: thesis: verum