let G be _Graph; :: thesis: ( G is edgeless iff for v, w being Vertex of G holds not v,w are_adjacent )

hereby :: thesis: ( ( for v, w being Vertex of G holds not v,w are_adjacent ) implies G is edgeless )

assume A1: G is edgeless ; :: thesis: for v, w being Vertex of G holds not v,w are_adjacent
let v, w be Vertex of G; :: thesis: not v,w are_adjacent
for e being object holds not e Joins v,w,G by A1, GLIB_008:50;
hence not v,w are_adjacent by CHORD:def 3; :: thesis: verum

end;

assume A2: for v, w being Vertex of G holds not v,w are_adjacent ; :: thesis: G is edgeless
assume not G is edgeless ; :: thesis: contradiction
then consider e being object such that
A3: e in the_Edges_of G by XBOOLE_0:def 1;
set v = (the_Source_of G) . e;
set w = (the_Target_of G) . e;
reconsider v = (the_Source_of G) . e, w = (the_Target_of G) . e as Vertex of G by A3, FUNCT_2:5;
e Joins v,w,G by A3, GLIB_000:def 13;
hence contradiction by A2, CHORD:def 3; :: thesis: verum