let G be SimpleGraph; :: thesis: for x being set st Vertices G = {x} holds
G = {{},{x}}
let a be set ; :: thesis: ( Vertices G = {a} implies G = {{},{a}} )
assume A: Vertices G = {a} ; :: thesis: G = {{},{a}}

B: now :: thesis: not Edges G <> {}

assume Edges G <> {} ; :: thesis: contradiction
then consider e being set such that
C: e in Edges G by XBOOLE_0:def 1;
consider x, y being set such that
D: x <> y and
E: x in Vertices G and
F: y in Vertices G and
e = {x,y} by C, SG4;
x = a by E, A, TARSKI:def 1;
hence contradiction by D, F, A, TARSKI:def 1; :: thesis: verum

end;

C: singletons (Vertices G) = {{a}} by A, Singletons0;
thus G = ({{}} \/ (singletons (Vertices G))) \/ (Edges G) by SG0
.= {{},{a}} by C, B, ENUMSET1:1 ; :: thesis: verum