let K be SimplicialComplexStr; :: thesis: Vertices K = union the topology of K

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: union the topology of K c= Vertices K

let x be object ; :: thesis: ( x in Vertices K implies x in union the topology of K )
assume A1: x in Vertices K ; :: thesis: x in union the topology of K
reconsider v = x as Element of K by A1;
v is vertex-like by A1, Def4;
then consider S being Subset of K such that
A2: S is simplex-like and
A3: v in S ;
S in the topology of K by A2;
hence x in union the topology of K by A3, TARSKI:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union the topology of K or x in Vertices K )
assume x in union the topology of K ; :: thesis: x in Vertices K
then consider y being set such that
A4: x in y and
A5: y in the topology of K by TARSKI:def 4;
reconsider y = y as Subset of K by A5;
y is simplex-like by A5;
hence x in Vertices K by A4, Lm3; :: thesis: verum