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