take [#] X ; :: thesis: x in Int ([#] X)
Int ([#] X) = [#] X by TOPS_1:15;
hence x in Int ([#] X) ; :: thesis: verum