take G = the simple complete n + 1 -vertex _Graph; :: thesis: ( G is simple & G is vertex-finite & G is n -regular )
( G is n +` 1 -vertex & G is vertex-finite ) ;
hence ( G is simple & G is vertex-finite & G is n -regular ) ; :: thesis: verum