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 A1: Vertices G = {a} ; :: thesis: G = {{},{a}}
A2: now :: thesis: not Edges G <> {}
assume Edges G <> {} ; :: thesis: contradiction
then consider e being object such that
A3: e in Edges G by XBOOLE_0:def 1;
consider x, y being set such that
A4: x <> y and
A5: x in Vertices G and
A6: y in Vertices G and
e = {x,y} by A3, Th11;
x = a by A5, A1, TARSKI:def 1;
hence contradiction by A4, A6, A1, TARSKI:def 1; :: thesis: verum
end;
A7: singletons (Vertices G) = {{a}} by A1, Th6;
thus G = ({{}} \/ (singletons (Vertices G))) \/ (Edges G) by Th27
.= {{},{a}} by A7, A2, ENUMSET1:1 ; :: thesis: verum