let G be loopless _Graph; :: thesis: ( G is edgeless iff for v, w being Vertex of G st v <> w holds
not v,w are_adjacent )
thus ( G is edgeless implies for v, w being Vertex of G st v <> w holds
not v,w are_adjacent ) by Th65; :: thesis: ( ( for v, w being Vertex of G st v <> w holds
not v,w are_adjacent ) implies G is edgeless )
assume A1: for v, w being Vertex of G st v <> w holds
not v,w are_adjacent ; :: thesis: G is edgeless
assume not G is edgeless ; :: thesis: contradiction
then consider e being object such that
A2: 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 A2, FUNCT_2:5;
A3: e Joins v,w,G by A2, GLIB_000:def 13;
then v <> w by GLIB_000:18;
hence contradiction by A1, A3, CHORD:def 3; :: thesis: verum