let X be set ; :: thesis: for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX holds Vertices SX c= Vertices KX
let KX be SimplicialComplexStr of X; :: thesis: for SX being SubSimplicialComplex of KX holds Vertices SX c= Vertices KX
let SX be SubSimplicialComplex of KX; :: thesis: Vertices SX c= Vertices KX
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Vertices SX or x in Vertices KX )
assume A1: x in Vertices SX ; :: thesis: x in Vertices KX
then reconsider v = x as Element of SX ;
v is vertex-like by A1, Def4;
then consider S being Subset of SX such that
A2: S is simplex-like and
A3: v in S ;
A4: the topology of SX c= the topology of KX by Def13;
A5: S in the topology of SX by A2;
then S in the topology of KX by A4;
then reconsider S = S as Subset of KX ;
v in S by A3;
then reconsider v = v as Element of KX ;
S is simplex-like by A4, A5;
then v is vertex-like by A3;
hence x in Vertices KX by Def4; :: thesis: verum