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