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