now :: thesis: ex v being Vertex of G st
( v .inDegree() = 0 & ( for w being Vertex of G holds v .inDegree() c= w .inDegree() ) )

take v = the Vertex of G; :: thesis: ( v .inDegree() = 0 & ( for w being Vertex of G holds v .inDegree() c= w .inDegree() ) )
thus v .inDegree() = 0 ; :: thesis: for w being Vertex of G holds v .inDegree() c= w .inDegree()
let w be Vertex of G; :: thesis: v .inDegree() c= w .inDegree()
thus v .inDegree() c= w .inDegree() ; :: thesis: verum

end;

hence G .minInDegree() is zero by Th37; :: thesis: verum