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