let V be RealLinearSpace; :: thesis: for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv & degree Kv <= 0 holds
TopStruct(# the carrier of Kv, the topology of Kv #) = BCS Kv
let Kv be non void SimplicialComplex of V; :: thesis: ( |.Kv.| c= [#] Kv & degree Kv <= 0 implies TopStruct(# the carrier of Kv, the topology of Kv #) = BCS Kv )
reconsider o = 1 as ExtReal ;
assume that
A1: |.Kv.| c= [#] Kv and
A2: degree Kv <= 0 ; :: thesis: TopStruct(# the carrier of Kv, the topology of Kv #) = BCS Kv
set B = center_of_mass V;
set BC = BCS Kv;
A3: BCS Kv = subdivision ((center_of_mass V),Kv) by A1, Def5;
then A4: [#] (BCS Kv) = [#] Kv by SIMPLEX0:def 20;
A5: dom (center_of_mass V) = (bool the carrier of V) \ {{}} by FUNCT_2:def 1;
A6: ( 0 + o = 0 + 1 & (degree Kv) + o <= 0 + o ) by A2, XXREAL_3:35, XXREAL_3:def 2;
A7: the topology of (BCS Kv) c= the topology of Kv

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of (BCS Kv) or x in the topology of Kv )
assume x in the topology of (BCS Kv) ; :: thesis: x in the topology of Kv
then reconsider X = x as Simplex of (BCS Kv) by PRE_TOPC:def 2;
reconsider X1 = X as Subset of Kv by A4;
consider S being c=-linear finite simplex-like Subset-Family of Kv such that
A8: X = (center_of_mass V) .: S by A3, SIMPLEX0:def 20;
A9: (center_of_mass V) .: S = (center_of_mass V) .: (S /\ (dom (center_of_mass V))) by RELAT_1:112;

per cases ( X is empty or not X is empty ) ;

suppose X is empty ; :: thesis: x in the topology of Kv

then X1 is simplex-like ;
hence x in the topology of Kv ; :: thesis: verum

end;

suppose A10: not X is empty ; :: thesis: x in the topology of Kv

then not S is empty by A8;
then union S in S by SIMPLEX0:9;
then reconsider U = union S as Simplex of Kv by TOPS_2:def 1;
A11: not U is empty

proof

assume A12: U is empty ; :: thesis: contradiction
S /\ (dom (center_of_mass V)) is empty

proof

assume not S /\ (dom (center_of_mass V)) is empty ; :: thesis: contradiction
then consider y being object such that
A13: y in S /\ (dom (center_of_mass V)) ;
reconsider y = y as set by TARSKI:1;
y in S by A13, XBOOLE_0:def 4;
then A14: y c= U by ZFMISC_1:74;
y <> {} by A13, ZFMISC_1:56;
hence contradiction by A12, A14; :: thesis: verum

end;

hence contradiction by A8, A9, A10; :: thesis: verum

end;

then A15: @ U in dom (center_of_mass V) by A5, ZFMISC_1:56;
card U <= (degree Kv) + 1 by SIMPLEX0:24;
then A16: card U <= 1 by A6, XXREAL_0:2;
card U >= 1 by A11, NAT_1:14;
then A17: card U = 1 by A16, XXREAL_0:1;
then consider u being object such that
A18: {u} = @ U by CARD_2:42;
u in {u} by TARSKI:def 1;
then reconsider u = u as Element of V by A18;
A19: S /\ (dom (center_of_mass V)) c= {U}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in S /\ (dom (center_of_mass V)) or y in {U} )
reconsider yy = y as set by TARSKI:1;
assume A20: y in S /\ (dom (center_of_mass V)) ; :: thesis: y in {U}
then y in S by XBOOLE_0:def 4;
then A21: yy c= U by ZFMISC_1:74;
y <> {} by A20, ZFMISC_1:56;
then y = U by A18, A21, ZFMISC_1:33;
hence y in {U} by TARSKI:def 1; :: thesis: verum

end;

not S /\ (dom (center_of_mass V)) is empty by A8, A9, A10;
then S /\ (dom (center_of_mass V)) = {U} by A19, ZFMISC_1:33;
then X = Im ((center_of_mass V),U) by A8, A9, RELAT_1:def 16
.= {((center_of_mass V) . U)} by A15, FUNCT_1:59
.= {((1 / 1) * (Sum {u}))} by A17, A18, RLAFFIN2:def 2
.= {(Sum {u})} by RLVECT_1:def 8
.= U by A18, RLVECT_2:9 ;
hence x in the topology of Kv by PRE_TOPC:def 2; :: thesis: verum

end;

end;

end;

the topology of Kv c= the topology of (BCS Kv)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of Kv or x in the topology of (BCS Kv) )
assume x in the topology of Kv ; :: thesis: x in the topology of (BCS Kv)
then reconsider X = x as Simplex of Kv by PRE_TOPC:def 2;
reconsider X1 = X as Subset of (BCS Kv) by A4;

per cases ( X is empty or not X is empty ) ;

suppose X is empty ; :: thesis: x in the topology of (BCS Kv)

then X1 is simplex-like ;
hence x in the topology of (BCS Kv) ; :: thesis: verum

end;

suppose A22: not X is empty ; :: thesis: x in the topology of (BCS Kv)

for Y being Subset of Kv st Y in {X} holds
Y is simplex-like by TARSKI:def 1;
then reconsider XX = {X} as finite simplex-like Subset-Family of Kv by TOPS_2:def 1;

now :: thesis: for x, y being set st x in XX & y in XX holds
x,y are_c=-comparable

let x, y be set ; :: thesis: ( x in XX & y in XX implies x,y are_c=-comparable )
assume that
A23: x in XX and
A24: y in XX ; :: thesis: x,y are_c=-comparable
x = X by A23, TARSKI:def 1;
hence x,y are_c=-comparable by A24, TARSKI:def 1; :: thesis: verum

end;

then A25: XX is c=-linear ;
card X <= (degree Kv) + 1 by SIMPLEX0:24;
then A26: card X <= 1 by A6, XXREAL_0:2;
card X >= 1 by A22, NAT_1:14;
then A27: card X = 1 by A26, XXREAL_0:1;
then consider u being object such that
A28: @ X = {u} by CARD_2:42;
A29: @ X in dom (center_of_mass V) by A5, A22, ZFMISC_1:56;
u in {u} by TARSKI:def 1;
then reconsider u = u as Element of V by A28;
(center_of_mass V) .: XX = Im ((center_of_mass V),X) by RELAT_1:def 16
.= {((center_of_mass V) . X)} by A29, FUNCT_1:59
.= {((1 / 1) * (Sum {u}))} by A27, A28, RLAFFIN2:def 2
.= {(Sum {u})} by RLVECT_1:def 8
.= X1 by A28, RLVECT_2:9 ;
then X1 is simplex-like by A3, A25, SIMPLEX0:def 20;
hence x in the topology of (BCS Kv) ; :: thesis: verum

end;

end;

end;

hence TopStruct(# the carrier of Kv, the topology of Kv #) = BCS Kv by A3, A4, A7, XBOOLE_0:def 10; :: thesis: verum