let n be Nat; :: thesis: for X being set
for A being affinely-independent Subset of (TOP-REAL n)
for E being Enumeration of A st not (dom E) \ X is empty holds
conv (E .: X) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X }
let X be set ; :: thesis: for A being affinely-independent Subset of (TOP-REAL n)
for E being Enumeration of A st not (dom E) \ X is empty holds
conv (E .: X) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X }
let A be affinely-independent Subset of (TOP-REAL n); :: thesis: for E being Enumeration of A st not (dom E) \ X is empty holds
conv (E .: X) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X }
let E be Enumeration of A; :: thesis: ( not (dom E) \ X is empty implies conv (E .: X) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X } )
assume A1: not (dom E) \ X is empty ; :: thesis: conv (E .: X) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X }
set d = dom E;
defpred S₁[ Nat] means ( $1 <> 0 implies for X being set st card ((dom E) \ X) = $1 holds
conv (A \ (E .: ((dom E) \ X))) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X } );
A2: rng E = A by RLAFFIN3:def 1;
A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

deffunc H₁( set ) -> Element of bool the carrier of (TOP-REAL n) = conv (A \ {(E . $1)});
let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
set i1 = i + 1;
assume i + 1 <> 0 ; :: thesis: for X being set st card ((dom E) \ X) = i + 1 holds
conv (A \ (E .: ((dom E) \ X))) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X }
let X be set ; :: thesis: ( card ((dom E) \ X) = i + 1 implies conv (A \ (E .: ((dom E) \ X))) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X } )
set U = { H₁(k) where k is Element of NAT : k in (dom E) \ X } ;
assume A5: card ((dom E) \ X) = i + 1 ; :: thesis: conv (A \ (E .: ((dom E) \ X))) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X }
then not (dom E) \ X is empty ;
then consider m being object such that
A6: m in (dom E) \ X by XBOOLE_0:def 1;
A7: m in dom E by A6, XBOOLE_0:def 5;
reconsider m = m as Element of NAT by A6;
A8: E .: {m} = Im (E,m) by RELAT_1:def 16
.= {(E . m)} by A7, FUNCT_1:59 ;

per cases ( i = 0 or i > 0 ) ;

suppose i = 0 ; :: thesis: conv (A \ (E .: ((dom E) \ X))) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X }

then consider x being object such that
A9: (dom E) \ X = {x} by A5, CARD_2:42;
A10: x = m by A6, A9, TARSKI:def 1;
A11: { H₁(k) where k is Element of NAT : k in (dom E) \ X } c= {H₁(m)}

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { H₁(k) where k is Element of NAT : k in (dom E) \ X } or u in {H₁(m)} )
assume u in { H₁(k) where k is Element of NAT : k in (dom E) \ X } ; :: thesis: u in {H₁(m)}
then ex k being Element of NAT st
( u = H₁(k) & k in (dom E) \ X ) ;
then u = H₁(m) by A9, A10, TARSKI:def 1;
hence u in {H₁(m)} by TARSKI:def 1; :: thesis: verum

end;

H₁(m) in { H₁(k) where k is Element of NAT : k in (dom E) \ X } by A6;
then A12: { H₁(k) where k is Element of NAT : k in (dom E) \ X } = {H₁(m)} by A11, ZFMISC_1:33;
E .: ((dom E) \ X) = {(E . m)} by A6, A8, A9, TARSKI:def 1;
hence conv (A \ (E .: ((dom E) \ X))) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X } by A12, SETFAM_1:10; :: thesis: verum

end;

suppose A13: i > 0 ; :: thesis: conv (A \ (E .: ((dom E) \ X))) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X }

set Xm = X \/ {m};
set Um = { H₁(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } ;
set t = the Element of (dom E) \ (X \/ {m});
A14: (((dom E) \ X) \ {m}) \/ {m} = (dom E) \ X by A6, ZFMISC_1:116;
A15: ((dom E) \ X) \ {m} = (dom E) \ (X \/ {m}) by XBOOLE_1:41;
A16: { H₁(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } c= { H₁(k) where k is Element of NAT : k in (dom E) \ X }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H₁(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } or x in { H₁(k) where k is Element of NAT : k in (dom E) \ X } )
assume x in { H₁(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } ; :: thesis: x in { H₁(k) where k is Element of NAT : k in (dom E) \ X }
then consider k being Element of NAT such that
A17: x = H₁(k) and
A18: k in (dom E) \ (X \/ {m}) ;
k in (dom E) \ X by A15, A14, A18, XBOOLE_0:def 3;
hence x in { H₁(k) where k is Element of NAT : k in (dom E) \ X } by A17; :: thesis: verum

end;

m in {m} by TARSKI:def 1;
then not m in ((dom E) \ X) \ {m} by XBOOLE_0:def 5;
then A19: (card (((dom E) \ X) \ {m})) + 1 = card ((dom E) \ X) by A14, CARD_2:41;
then not (dom E) \ (X \/ {m}) is empty by A5, A13, A15;
then the Element of (dom E) \ (X \/ {m}) in (dom E) \ (X \/ {m}) ;
then A20: H₁( the Element of (dom E) \ (X \/ {m})) in { H₁(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } ;
set c = H₁(m);
set CC = {H₁(m)};
set CA = Complex_of {A};
A21: the topology of (Complex_of {A}) = bool A by SIMPLEX0:4;
A22: { H₁(k) where k is Element of NAT : k in (dom E) \ X } c= { H₁(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } \/ {H₁(m)}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H₁(k) where k is Element of NAT : k in (dom E) \ X } or x in { H₁(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } \/ {H₁(m)} )
assume x in { H₁(k) where k is Element of NAT : k in (dom E) \ X } ; :: thesis: x in { H₁(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } \/ {H₁(m)}
then consider k being Element of NAT such that
A23: x = H₁(k) and
A24: k in (dom E) \ X ;
( k in (dom E) \ (X \/ {m}) or k in {m} ) by A15, A14, A24, XBOOLE_0:def 3;
then ( k in (dom E) \ (X \/ {m}) or k = m ) by TARSKI:def 1;
then ( x in { H₁(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } or x in {H₁(m)} ) by A23, TARSKI:def 1;
hence x in { H₁(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } \/ {H₁(m)} by XBOOLE_0:def 3; :: thesis: verum

end;

H₁(m) in { H₁(k) where k is Element of NAT : k in (dom E) \ X } by A6;
then {H₁(m)} c= { H₁(k) where k is Element of NAT : k in (dom E) \ X } by ZFMISC_1:31;
then A25: { H₁(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } \/ {H₁(m)} c= { H₁(k) where k is Element of NAT : k in (dom E) \ X } by A16, XBOOLE_1:8;
reconsider A1 = A \ (E .: ((dom E) \ (X \/ {m}))), A2 = A \ {(E . m)} as Subset of (Complex_of {A}) ;
A \ {(E . m)} c= A by XBOOLE_1:36;
then A26: A2 is simplex-like by A21, PRE_TOPC:def 2;
A \ (E .: ((dom E) \ (X \/ {m}))) c= A by XBOOLE_1:36;
then A1 is simplex-like by A21, PRE_TOPC:def 2;
then A27: (conv (@ A1)) /\ (conv (@ A2)) = conv (@ (A1 /\ A2)) by A26, SIMPLEX1:def 8;
(E .: ((dom E) \ (X \/ {m}))) \/ {(E . m)} = E .: (((dom E) \ (X \/ {m})) \/ {m}) by A8, RELAT_1:120
.= E .: ((dom E) \ X) by A14, XBOOLE_1:41 ;
then A28: A1 /\ A2 = A \ (E .: ((dom E) \ X)) by XBOOLE_1:53;
conv (A \ (E .: ((dom E) \ (X \/ {m})))) = meet { H₁(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } by A4, A5, A13, A15, A19;
then conv (A \ (E .: ((dom E) \ X))) = (meet { H₁(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } ) /\ (meet {H₁(m)}) by A28, A27, SETFAM_1:10
.= meet ( { H₁(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } \/ {H₁(m)}) by A20, SETFAM_1:9 ;
hence conv (A \ (E .: ((dom E) \ X))) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X } by A25, A22, XBOOLE_0:def 10; :: thesis: verum

end;

end;

end;

A29: S₁[ 0 ] ;
for i being Nat holds S₁[i] from NAT_1:sch 2(A29, A3);
then A30: S₁[ card ((dom E) \ X)] ;
(dom E) \ ((dom E) \ X) = (dom E) /\ X by XBOOLE_1:48;
then E .: X = E .: ((dom E) \ ((dom E) \ X)) by RELAT_1:112
.= (E .: (dom E)) \ (E .: ((dom E) \ X)) by FUNCT_1:64
.= A \ (E .: ((dom E) \ X)) by A2, RELAT_1:113 ;
hence conv (E .: X) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X } by A1, A30; :: thesis: verum