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 )

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

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

now

assume u .edgesInOut() <> {} ; :: thesis: contradiction
then consider e being set 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: now

A5: e in the_Edges_of G by A3, GLIB_000:def 13;
assume A6: u = v ; :: thesis: contradiction
then A7: (the_Target_of G) . e = u by A3, GLIB_000:def 13;
(the_Source_of G) . e = u by A3, A6, GLIB_000:def 13;
hence contradiction by A5, A7, GLIB_000:def 18; :: thesis: verum

end;

v,u are_adjacent by A3, Def3;
hence contradiction by A1, A4, Th52; :: thesis: verum

end;

hence u is isolated by GLIB_000:def 49; :: thesis: verum

end;

assume u is isolated ; :: thesis: G .AdjacentSet {u} = {}
then A8: u .edgesInOut() = {} by GLIB_000:def 49;

now

let v be set ; :: thesis: not v in G .AdjacentSet {u}
assume A9: v in G .AdjacentSet {u} ; :: thesis: contradiction
reconsider v = v as Vertex of G by A9;
v,u are_adjacent by A9, Th52;
then ex e being set st e Joins v,u,G by Def3;
hence contradiction by A8, GLIB_000:14, GLIB_000:62; :: thesis: verum

end;

hence G .AdjacentSet {u} = {} by XBOOLE_0:def 1; :: thesis: verum