take the empty TopStruct ; :: thesis: [#] the empty TopStruct c= X
thus [#] the empty TopStruct c= X ; :: thesis: verum