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