let V be non empty set ; :: thesis: for E being Relation of V
for v being Vertex of (createGraph (V,E)) holds
( v is isolated iff not v in field E )
let E be Relation of V; :: thesis: for v being Vertex of (createGraph (V,E)) holds
( v is isolated iff not v in field E )
let v be Vertex of (createGraph (V,E)); :: thesis: ( v is isolated iff not v in field E )

hereby :: thesis: ( not v in field E implies v is isolated )

assume A1: v is isolated ; :: thesis: not v in field E
assume v in field E ; :: thesis: contradiction
then v in (dom E) \/ (rng E) by RELAT_1:def 6;

per cases then ( v in dom E or v in rng E ) by XBOOLE_0:def 3;

suppose v in dom E ; :: thesis: contradiction

then consider w being object such that
A2: [v,w] in E by XTUPLE_0:def 12;
thus contradiction by A1, A2, Th63, GLIB_000:144; :: thesis: verum

end;

suppose v in rng E ; :: thesis: contradiction

then consider w being object such that
A3: [w,v] in E by XTUPLE_0:def 13;
thus contradiction by A1, A3, Th63, GLIB_000:144; :: thesis: verum

end;

end;

end;

assume A4: not v in field E ; :: thesis: v is isolated
assume not v is isolated ; :: thesis: contradiction
then v .edgesInOut() <> {} by GLIB_000:def 49;
then consider e being object such that
A5: e in v .edgesInOut() by XBOOLE_0:def 1;
e in (v .edgesIn()) \/ (v .edgesOut()) by A5, GLIB_000:60;

per cases then ( e in v .edgesIn() or e in v .edgesOut() ) by XBOOLE_0:def 3;

suppose e in v .edgesIn() ; :: thesis: contradiction

then consider w being set such that
A6: e DJoins w,v, createGraph (V,E) by GLIB_000:57;
e = [w,v] by A6, Th64;
then [w,v] in E by A6, Th63;
hence contradiction by A4, RELAT_1:15; :: thesis: verum

end;

suppose e in v .edgesOut() ; :: thesis: contradiction

then consider w being set such that
A7: e DJoins v,w, createGraph (V,E) by GLIB_000:59;
e = [v,w] by A7, Th64;
then [v,w] in E by A7, Th63;
hence contradiction by A4, RELAT_1:15; :: thesis: verum

end;

end;