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;
A2: ex u being Vertex of G st
( x = u & not u in {v} & 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;
v = w by A3, TARSKI:def 1;
hence contradiction by A2, A3; :: thesis: verum

end;

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