let G be loopless _Graph; :: thesis: for u being Vertex of G holds

( G .AdjacentSet {u} = {} iff u is isolated )

let u be Vertex of G; :: thesis: ( G .AdjacentSet {u} = {} iff u is isolated )

then A5: u .edgesInOut() = {} ;

( G .AdjacentSet {u} = {} iff u is isolated )

let u be Vertex of G; :: thesis: ( G .AdjacentSet {u} = {} iff u is isolated )

hereby :: thesis: ( u is isolated implies G .AdjacentSet {u} = {} )

assume
u is isolated
; :: thesis: G .AdjacentSet {u} = {} assume A1:
G .AdjacentSet {u} = {}
; :: thesis: u is isolated

end;now :: thesis: not u .edgesInOut() <> {}

hence
u is isolated
; :: thesis: verumassume
u .edgesInOut() <> {}
; :: thesis: contradiction

then consider e being object such that

A2: e in u .edgesInOut() by XBOOLE_0:def 1;

consider v being Vertex of G such that

A3: e Joins u,v,G by A2, GLIB_000:64;

A4: u <> v by A3, GLIB_000:def 18;

v,u are_adjacent by A3, Def3;

hence contradiction by A1, A4, Th51; :: thesis: verum

end;then consider e being object such that

A2: e in u .edgesInOut() by XBOOLE_0:def 1;

consider v being Vertex of G such that

A3: e Joins u,v,G by A2, GLIB_000:64;

A4: u <> v by A3, GLIB_000:def 18;

v,u are_adjacent by A3, Def3;

hence contradiction by A1, A4, Th51; :: thesis: verum

then A5: u .edgesInOut() = {} ;

now :: thesis: for v being object holds not v in G .AdjacentSet {u}

hence
G .AdjacentSet {u} = {}
by XBOOLE_0:def 1; :: thesis: verumlet v be object ; :: thesis: not v in G .AdjacentSet {u}

assume A6: v in G .AdjacentSet {u} ; :: thesis: contradiction

reconsider v = v as Vertex of G by A6;

v,u are_adjacent by A6, Th51;

then ex e being object st e Joins v,u,G ;

hence contradiction by A5, GLIB_000:14, GLIB_000:62; :: thesis: verum

end;assume A6: v in G .AdjacentSet {u} ; :: thesis: contradiction

reconsider v = v as Vertex of G by A6;

v,u are_adjacent by A6, Th51;

then ex e being object st e Joins v,u,G ;

hence contradiction by A5, GLIB_000:14, GLIB_000:62; :: thesis: verum