let G be _Graph; :: thesis: for v being Vertex of G holds
( v is isolated iff not v in (rng (the_Source_of G)) \/ (rng (the_Target_of G)) )
let v be Vertex of G; :: thesis: ( v is isolated iff not v in (rng (the_Source_of G)) \/ (rng (the_Target_of G)) )

hereby :: thesis: ( not v in (rng (the_Source_of G)) \/ (rng (the_Target_of G)) implies v is isolated )

assume A1: v is isolated ; :: thesis: not v in (rng (the_Source_of G)) \/ (rng (the_Target_of G))
assume v in (rng (the_Source_of G)) \/ (rng (the_Target_of G)) ; :: thesis: contradiction

per cases then ( v in rng (the_Source_of G) or v in rng (the_Target_of G) ) by XBOOLE_0:def 3;

suppose v in rng (the_Source_of G) ; :: thesis: contradiction

then consider e being object such that
A2: ( e in dom (the_Source_of G) & (the_Source_of G) . e = v ) by FUNCT_1:def 3;
e DJoins v,(the_Target_of G) . e,G by A2;
hence contradiction by A1, Th144; :: thesis: verum

end;

suppose v in rng (the_Target_of G) ; :: thesis: contradiction

then consider e being object such that
A3: ( e in dom (the_Target_of G) & (the_Target_of G) . e = v ) by FUNCT_1:def 3;
e DJoins (the_Source_of G) . e,v,G by A3;
hence contradiction by A1, Th144; :: thesis: verum

end;

end;

end;

assume A4: not v in (rng (the_Source_of G)) \/ (rng (the_Target_of G)) ; :: thesis: v is isolated
assume not v is isolated ; :: thesis: contradiction
then v .edgesInOut() <> {} ;
then consider e being object such that
A5: e in v .edgesInOut() by XBOOLE_0:def 1;
A6: ( e in the_Edges_of G & ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) ) by A5, Th61;

per cases then ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) ;

suppose A7: (the_Source_of G) . e = v ; :: thesis: contradiction

e in dom (the_Source_of G) by A6, FUNCT_2:def 1;
then v in rng (the_Source_of G) by A7, FUNCT_1:3;
hence contradiction by A4, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A8: (the_Target_of G) . e = v ; :: thesis: contradiction

e in dom (the_Target_of G) by A6, FUNCT_2:def 1;
then v in rng (the_Target_of G) by A8, FUNCT_1:3;
hence contradiction by A4, XBOOLE_0:def 3; :: thesis: verum

end;

end;