take the simple 1 -regular _Graph ; :: thesis: ( the simple 1 -regular _Graph is simple & not the simple 1 -regular _Graph is edgeless & the simple 1 -regular _Graph is finite & the simple 1 -regular _Graph is regular )
thus ( the simple 1 -regular _Graph is simple & not the simple 1 -regular _Graph is edgeless & the simple 1 -regular _Graph is finite & the simple 1 -regular _Graph is regular ) ; :: thesis: verum