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