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))

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 )
;

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;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