let G2 be _Graph; :: thesis: for V being set
for G1 being addVertices of G2,V st V \ (the_Vertices_of G2) <> {} holds
( G1 .minDegree() = 0 & G1 .minInDegree() = 0 & G1 .minOutDegree() = 0 )
let V be set ; :: thesis: for G1 being addVertices of G2,V st V \ (the_Vertices_of G2) <> {} holds
( G1 .minDegree() = 0 & G1 .minInDegree() = 0 & G1 .minOutDegree() = 0 )
let G1 be addVertices of G2,V; :: thesis: ( V \ (the_Vertices_of G2) <> {} implies ( G1 .minDegree() = 0 & G1 .minInDegree() = 0 & G1 .minOutDegree() = 0 ) )
assume V \ (the_Vertices_of G2) <> {} ; :: thesis: ( G1 .minDegree() = 0 & G1 .minInDegree() = 0 & G1 .minOutDegree() = 0 )
then consider v being object such that
A1: v in V \ (the_Vertices_of G2) by XBOOLE_0:def 1;
reconsider v = v as Vertex of G1 by A1, GLIB_006:86;
v is isolated by A1, GLIB_006:88;
hence ( G1 .minDegree() = 0 & G1 .minInDegree() = 0 & G1 .minOutDegree() = 0 ) by Th46; :: thesis: verum