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