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:
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 ;
A4: u <> v by ;
v,u are_adjacent by ;
hence contradiction by A1, A4, Th51; :: thesis: verum
end;
hence u is isolated ; :: thesis: verum
end;
assume u is isolated ; :: thesis:
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 ;
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