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 :: thesis: not u .edgesInOut() <> {}

assume 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;

hence u is isolated ; :: thesis: verum

end;

assume u is isolated ; :: thesis: G .AdjacentSet {u} = {}
then A5: u .edgesInOut() = {} ;

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

let 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;

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