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 by GLIB_000:16;
hence contradiction by A1, Th25; :: thesis: verum
end;
suppose e DJoins w,v,G ; :: thesis: contradiction
then e Joins v,w,G by GLIB_000:16;
hence contradiction by A1, Th25; :: thesis: verum
end;
end;