support (SMoebius X) = X /\ SCNAT by Def5;
hence SMoebius X is finite-support by PRE_POLY:def 8; :: thesis: verum