take {0 } ; :: thesis: ( {0 } is trivial & not {0 } is empty )
thus ( {0 } is trivial & not {0 } is empty ) ; :: thesis: verum