set G = the trivial simple _Graph;

take the trivial simple _Graph ; :: thesis: ( the trivial simple _Graph is trivial & the trivial simple _Graph is simple & the trivial simple _Graph is complete )

thus ( the trivial simple _Graph is trivial & the trivial simple _Graph is simple & the trivial simple _Graph is complete ) ; :: thesis: verum

take the trivial simple _Graph ; :: thesis: ( the trivial simple _Graph is trivial & the trivial simple _Graph is simple & the trivial simple _Graph is complete )

thus ( the trivial simple _Graph is trivial & the trivial simple _Graph is simple & the trivial simple _Graph is complete ) ; :: thesis: verum