let n, k be Nat; :: thesis: for Affn being affinely-independent Subset of (TOP-REAL n)

for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn

for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds

( Ak is open iff B is open )

let Affn be affinely-independent Subset of (TOP-REAL n); :: thesis: for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn

for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds

( Ak is open iff B is open )

let Ak be Subset of (TOP-REAL k); :: thesis: for EN being Enumeration of Affn

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

set BB = { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } ;

A3: [#] ((TOP-REAL n) | (Affin Affn)) = Affin Affn by PRE_TOPC:def 5;

A4: { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } c= B

B c= { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) }

A9: rng EN = Affn by Def1;

then A10: len EN = card Affn by FINSEQ_4:62;

then A11: len EN >= 1 by A1, NAT_1:14;

then A12: len EN in dom EN by FINSEQ_3:25;

then EN . (len EN) in Affn by A9, FUNCT_1:def 3;

then reconsider EL = EN . (len EN) as Element of (TOP-REAL n) ;

len EN in Seg (card Affn) by A10, A11;

then A13: ((card Affn) |-> (- EL)) . (len EN) = - EL by FINSEQ_2:57;

A14: k < card ((- EL) + Affn) by A1, RLAFFIN1:7;

set T = transl ((- EL),(TOP-REAL n));

set TAA = (transl ((- EL),(TOP-REAL n))) .: (Affin Affn);

A15: [#] ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) = (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) by PRE_TOPC:def 5;

A16: rng ((transl ((- EL),(TOP-REAL n))) | (Affin Affn)) = (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) by RELAT_1:115;

A17: dom (transl ((- EL),(TOP-REAL n))) = [#] (TOP-REAL n) by FUNCT_2:52;

then dom ((transl ((- EL),(TOP-REAL n))) | (Affin Affn)) = Affin Affn by RELAT_1:62;

then reconsider TA = (transl ((- EL),(TOP-REAL n))) | (Affin Affn) as Function of ((TOP-REAL n) | (Affin Affn)),((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) by A3, A15, A16, FUNCT_2:1;

reconsider TAB = TA .: B as Subset of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (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 A19, FINSEQ_4:62;

then dom EN = dom Ev by A10, FINSEQ_3:29;

then Ev . (len EN) = EL + (- EL) by A12, A13, FVSUM_1:17

.= 0. (TOP-REAL n) by RLVECT_1:5

.= 0* n by EUCLID:70 ;

then A22: Ev . (len Ev) = 0* n by A10, A19, A21, FINSEQ_4:62;

set Tab = { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak } ;

A23: (- EL) + (Affin Affn) = Affin ((- EL) + Affn) by RLAFFIN1:53;

then A24: (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) = Affin ((- EL) + Affn) by RLTOPSP1:33;

TA .: B = (transl ((- EL),(TOP-REAL n))) .: B by A3, RELAT_1:129;

then A25: TAB = { w where w is Element of (TOP-REAL n) : ( w in Affin ((- EL) + Affn) & (w |-- Ev) | k in Ak ) } by A8, Lm6;

A26: TAB c= { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak }

{ w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak } c= TAB

then ( TAB is open iff Ak is open ) by A24, A22, A14, A20, Lm8;

hence ( Ak is open iff B is open ) by A6, A18, A30, TOPGRP_1:25; :: thesis: verum

for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn

for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds

( Ak is open iff B is open )

let Affn be affinely-independent Subset of (TOP-REAL n); :: thesis: for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn

for B being Subset of ((TOP-REAL n) | (Affin Affn)) st k < card Affn & B = { pnA where pnA is Element of ((TOP-REAL n) | (Affin Affn)) : (pnA |-- EN) | k in Ak } holds

( Ak is open iff B is open )

let Ak be Subset of (TOP-REAL k); :: thesis: for EN being Enumeration of Affn

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

set BB = { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } ;

A3: [#] ((TOP-REAL n) | (Affin Affn)) = Affin Affn by PRE_TOPC:def 5;

A4: { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } c= B

proof

A6:
not Affn is empty
by A1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } or x in B )

assume x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } ; :: thesis: x in B

then consider u being Element of (TOP-REAL n) 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;assume x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } ; :: thesis: x in B

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

A5: ( x = u & u in Affin Affn & (u |-- EN) | k in Ak ) ;

thus x in B by A2, A3, A5; :: thesis: verum

B c= { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) }

proof

then A8:
{ u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } = B
by A4;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } )

assume x in B ; :: thesis: x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) }

then consider u being Element of ((TOP-REAL n) | (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 (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } by A7; :: thesis: verum

end;assume x in B ; :: thesis: x in { u where u is Element of (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) }

then consider u being Element of ((TOP-REAL n) | (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 (TOP-REAL n) : ( u in Affin Affn & (u |-- EN) | k in Ak ) } by A7; :: thesis: verum

A9: rng EN = Affn by Def1;

then A10: len EN = card Affn by FINSEQ_4:62;

then A11: len EN >= 1 by A1, NAT_1:14;

then A12: len EN in dom EN by FINSEQ_3:25;

then EN . (len EN) in Affn by A9, FUNCT_1:def 3;

then reconsider EL = EN . (len EN) as Element of (TOP-REAL n) ;

len EN in Seg (card Affn) by A10, A11;

then A13: ((card Affn) |-> (- EL)) . (len EN) = - EL by FINSEQ_2:57;

A14: k < card ((- EL) + Affn) by A1, RLAFFIN1:7;

set T = transl ((- EL),(TOP-REAL n));

set TAA = (transl ((- EL),(TOP-REAL n))) .: (Affin Affn);

A15: [#] ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) = (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) by PRE_TOPC:def 5;

A16: rng ((transl ((- EL),(TOP-REAL n))) | (Affin Affn)) = (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) by RELAT_1:115;

A17: dom (transl ((- EL),(TOP-REAL n))) = [#] (TOP-REAL n) by FUNCT_2:52;

then dom ((transl ((- EL),(TOP-REAL n))) | (Affin Affn)) = Affin Affn by RELAT_1:62;

then reconsider TA = (transl ((- EL),(TOP-REAL n))) | (Affin Affn) as Function of ((TOP-REAL n) | (Affin Affn)),((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) by A3, A15, A16, FUNCT_2:1;

reconsider TAB = TA .: B as Subset of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (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 A19, FINSEQ_4:62;

then dom EN = dom Ev by A10, FINSEQ_3:29;

then Ev . (len EN) = EL + (- EL) by A12, A13, FVSUM_1:17

.= 0. (TOP-REAL n) by RLVECT_1:5

.= 0* n by EUCLID:70 ;

then A22: Ev . (len Ev) = 0* n by A10, A19, A21, FINSEQ_4:62;

set Tab = { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak } ;

A23: (- EL) + (Affin Affn) = Affin ((- EL) + Affn) by RLAFFIN1:53;

then A24: (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) = Affin ((- EL) + Affn) by RLTOPSP1:33;

TA .: B = (transl ((- EL),(TOP-REAL n))) .: B by A3, RELAT_1:129;

then A25: TAB = { w where w is Element of (TOP-REAL n) : ( w in Affin ((- EL) + Affn) & (w |-- Ev) | k in Ak ) } by A8, Lm6;

A26: TAB c= { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak }

proof

A30:
not (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) is empty
by A6, A17, RELAT_1:119;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in TAB or x in { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak } )

assume x in TAB ; :: thesis: x in { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak }

then consider w being Element of (TOP-REAL n) 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),(TOP-REAL n))) .: (Affin Affn) by A23, A28, RLTOPSP1:33;

hence x in { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak } by A15, A27, A29; :: thesis: verum

end;assume x in TAB ; :: thesis: x in { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak }

then consider w being Element of (TOP-REAL n) 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),(TOP-REAL n))) .: (Affin Affn) by A23, A28, RLTOPSP1:33;

hence x in { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak } by A15, A27, A29; :: thesis: verum

{ w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak } c= TAB

proof

then
TAB = { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak }
by A26;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak } or x in TAB )

assume x in { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak } ; :: thesis: x in TAB

then consider w being Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) such that

A31: ( x = w & (w |-- Ev) | k in Ak ) ;

w in (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) by A15, A30;

hence x in TAB by A24, A25, A31; :: thesis: verum

end;assume x in { w where w is Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) : (w |-- Ev) | k in Ak } ; :: thesis: x in TAB

then consider w being Element of ((TOP-REAL n) | ((transl ((- EL),(TOP-REAL n))) .: (Affin Affn))) such that

A31: ( x = w & (w |-- Ev) | k in Ak ) ;

w in (transl ((- EL),(TOP-REAL n))) .: (Affin Affn) by A15, A30;

hence x in TAB by A24, A25, A31; :: thesis: verum

then ( TAB is open iff Ak is open ) by A24, A22, A14, A20, Lm8;

hence ( Ak is open iff B is open ) by A6, A18, A30, TOPGRP_1:25; :: thesis: verum