let G be _trivial _Graph; :: thesis: for v being Vertex of G holds
( v .inDegree() = G .size() & v .outDegree() = G .size() & v .degree() = (G .size()) +` (G .size()) )
let v be Vertex of G; :: thesis: ( v .inDegree() = G .size() & v .outDegree() = G .size() & v .degree() = (G .size()) +` (G .size()) )
thus ( v .inDegree() = G .size() & v .outDegree() = G .size() ) by Th30; :: thesis: v .degree() = (G .size()) +` (G .size())
hence v .degree() = (G .size()) +` (G .size()) ; :: thesis: verum