let G be _Graph; :: thesis: for v being Vertex of G
for e, w being object st v is isolated holds
( not e DJoins v,w,G & not e DJoins w,v,G )
let v be Vertex of G; :: thesis: for e, w being object st v is isolated holds
( not e DJoins v,w,G & not e DJoins w,v,G )
let e, w be object ; :: thesis: ( v is isolated implies ( not e DJoins v,w,G & not e DJoins w,v,G ) )
assume A1: v is isolated ; :: thesis: ( not e DJoins v,w,G & not e DJoins w,v,G )
assume ( e DJoins v,w,G or e DJoins w,v,G ) ; :: thesis: contradiction

per cases then ( e DJoins v,w,G or e DJoins w,v,G ) ;

suppose e DJoins v,w,G ; :: thesis: contradiction

then e Joins v,w,G ;
hence contradiction by A1, Th143; :: thesis: verum

end;

suppose e DJoins w,v,G ; :: thesis: contradiction

then e Joins v,w,G ;
hence contradiction by A1, Th143; :: thesis: verum

end;

end;