let n be Nat; :: thesis: for V being RealLinearSpace
for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds
Vertices Kv c= Vertices (BCS (n,Kv))
let V be RealLinearSpace; :: thesis: for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds
Vertices Kv c= Vertices (BCS (n,Kv))
let Kv be non void SimplicialComplex of V; :: thesis: ( |.Kv.| c= [#] Kv implies Vertices Kv c= Vertices (BCS (n,Kv)) )
set S = Skeleton_of (Kv,0);
assume A1: |.Kv.| c= [#] Kv ; :: thesis: Vertices Kv c= Vertices (BCS (n,Kv))

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

suppose n = 0 ; :: thesis: Vertices Kv c= Vertices (BCS (n,Kv))

hence Vertices Kv c= Vertices (BCS (n,Kv)) by A1, Th16; :: thesis: verum

end;

suppose A2: n > 0 ; :: thesis: Vertices Kv c= Vertices (BCS (n,Kv))

the topology of (Skeleton_of (Kv,0)) c= the topology of Kv by SIMPLEX0:def 13;
then |.(Skeleton_of (Kv,0)).| c= |.Kv.| by Th4;
then A3: |.(Skeleton_of (Kv,0)).| c= [#] (Skeleton_of (Kv,0)) by A1;
then ( degree (Skeleton_of (Kv,0)) <= 0 & BCS (n,(Skeleton_of (Kv,0))) is SubSimplicialComplex of BCS (n,Kv) ) by A1, Th23, SIMPLEX0:44;
then Skeleton_of (Kv,0) is SubSimplicialComplex of BCS (n,Kv) by A2, A3, Th22;
then A4: Vertices (Skeleton_of (Kv,0)) c= Vertices (BCS (n,Kv)) by SIMPLEX0:31;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Vertices Kv or x in Vertices (BCS (n,Kv)) )
assume A5: x in Vertices Kv ; :: thesis: x in Vertices (BCS (n,Kv))
then reconsider v = x as Element of Kv ;
v is vertex-like by A5, SIMPLEX0:def 4;
then consider A being Subset of Kv such that
A6: A is simplex-like and
A7: v in A ;
reconsider vv = {v} as Subset of Kv by A7, ZFMISC_1:31;
{v} c= A by A7, ZFMISC_1:31;
then vv is simplex-like by A6, MATROID0:1;
then A8: vv in the topology of Kv ;
( card vv = 1 & card 1 = 1 ) by CARD_1:30;
then vv in the_subsets_with_limited_card (1, the topology of Kv) by A8, SIMPLEX0:def 2;
then vv in the topology of (Skeleton_of (Kv,0)) by SIMPLEX0:2;
then reconsider vv = vv as Simplex of (Skeleton_of (Kv,0)) by PRE_TOPC:def 2;
A9: v in vv by TARSKI:def 1;
reconsider v = v as Element of (Skeleton_of (Kv,0)) ;
v is vertex-like by A9;
then v in Vertices (Skeleton_of (Kv,0)) by SIMPLEX0:def 4;
hence x in Vertices (BCS (n,Kv)) by A4; :: thesis: verum

end;

end;