reconsider ZERO = 0 as Integer ;
0 > 0 - 1 ;
then 0 -' 1 = 0 by XREAL_0:def 2;
then A1: Radix (0 -' 1) = 1 by POWER:24;
ZERO is Element of INT by INT_1:def 2;
hence 0 in 0 -SD_Sub_S by A1; :: thesis: verum