let G be trivial _Graph; :: thesis: for v being Vertex of G holds v is simplicial
let v be Vertex of G; :: thesis: v is simplicial

now

assume G .AdjacentSet {v} <> {} ; :: thesis: contradiction
then consider x being set such that
A1: x in G .AdjacentSet {v} by XBOOLE_0:def 1;
consider u being Vertex of G such that
x = u and
A2: not u in {v} and
ex v1 being Vertex of G st
( v1 in {v} & u,v1 are_adjacent ) by A1;
consider w being Vertex of G such that
A3: the_Vertices_of G = {w} by GLIB_000:25;
( u = w & v = w ) by A3, TARSKI:def 1;
hence contradiction by A2, TARSKI:def 1; :: thesis: verum

end;

hence v is simplicial by Def7; :: thesis: verum