let v be Vertex of G; :: thesis: ( v is isolated implies ( v is with_min_degree & v is with_min_in_degree & v is with_min_out_degree ) )
assume A6: v is isolated ; :: thesis: ( v is with_min_degree & v is with_min_in_degree & v is with_min_out_degree )
then ( G .minDegree() = 0 & G .minInDegree() = 0 & G .minOutDegree() = 0 ) by Th46;
hence ( v is with_min_degree & v is with_min_in_degree & v is with_min_out_degree ) by A6, GLIBPRE0:35, GLIBPRE0:34; :: thesis: verum