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 ((),Kv) by ;
then A4: [#] (BCS Kv) = [#] Kv by SIMPLEX0:def 20;
A5: dom () = (bool the carrier of V) \ by FUNCT_2:def 1;
A6: ( 0 + o = 0 + 1 & (degree Kv) + o <= 0 + o ) by ;
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 = () .: S by ;
A9: (center_of_mass V) .: S = () .: (S /\ ()) by RELAT_1:112;
per cases ( X is empty or not X is empty ) ;
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 /\ () is empty
proof
assume not S /\ () is empty ; :: thesis: contradiction
then consider y being object such that
A13: y in S /\ () ;
reconsider y = y as set by TARSKI:1;
y in S by ;
then A14: y c= U by ZFMISC_1:74;
y <> {} by ;
hence contradiction by A12, A14; :: thesis: verum
end;
hence contradiction by A8, A9, A10; :: thesis: verum
end;
then A15: @ U in dom () by ;
card U <= (degree Kv) + 1 by SIMPLEX0:24;
then A16: card U <= 1 by ;
card U >= 1 by ;
then A17: card U = 1 by ;
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 /\ () c= {U}
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in S /\ () or y in {U} )
reconsider yy = y as set by TARSKI:1;
assume A20: y in S /\ () ; :: thesis: y in {U}
then y in S by XBOOLE_0:def 4;
then A21: yy c= U by ZFMISC_1:74;
y <> {} by ;
then y = U by ;
hence y in {U} by TARSKI:def 1; :: thesis: verum
end;
not S /\ () is empty by A8, A9, A10;
then S /\ () = {U} by ;
then X = Im ((),U) by
.= {(() . U)} by
.= {((1 / 1) * ())} by
.= {()} by RLVECT_1:def 8
.= U by ;
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 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 = X by ;
hence x,y are_c=-comparable by ; :: thesis: verum
end;
then A25: XX is c=-linear ;
card X <= (degree Kv) + 1 by SIMPLEX0:24;
then A26: card X <= 1 by ;
card X >= 1 by ;
then A27: card X = 1 by ;
then consider u being object such that
A28: @ X = {u} by CARD_2:42;
A29: @ X in dom () by ;
u in {u} by TARSKI:def 1;
then reconsider u = u as Element of V by A28;
() .: XX = Im ((),X) by RELAT_1:def 16
.= {(() . X)} by
.= {((1 / 1) * ())} by
.= {()} by RLVECT_1:def 8
.= X1 by ;
then X1 is simplex-like by ;
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 ; :: thesis: verum