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:67;

now

assume u = v ; :: thesis: contradiction
then ( e in the_Edges_of G & (the_Source_of G) . e = u & (the_Target_of G) . e = u ) by A3, GLIB_000:def 15;
hence contradiction by GLIB_000:def 20; :: thesis: verum

end;

then ( u <> v & v,u are_adjacent ) by A3, Def3;
hence contradiction by A1, Th52; :: thesis: verum

end;

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

end;

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

now

let v be set ; :: thesis: not v in G .AdjacentSet {u}
assume A5: v in G .AdjacentSet {u} ; :: thesis: contradiction
reconsider v = v as Vertex of G by A5;
v,u are_adjacent by A5, Th52;
then consider e being set such that
A6: e Joins v,u,G by Def3;
thus contradiction by A4, A6, GLIB_000:17, GLIB_000:65; :: thesis: verum

end;

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