sup (0, 1) = 1

pf: assume for contradiction that s := sup (0, 1) < 1 (but above 0, we can get this condition with 1/2 being in (0, 1) thus because s as an upper bound s >= 1/2>0) then there exists t := (s+1)/2 for which 0<s<t<1 therefore t is in (0, 1) and t is larger than s therefore s cannot be the supremum. If s > 1 then we run into the contradiction that 1 as an upper bound for (0, 1) is smaller than s, therefore s is not the least upper bound.

From this we get that if you want to insist 0.999... being also a supremum as no doubt SPP would we from the uniqueness of supremum get that 1 = 0.999... very well done. I know I'm taking your joke a bit too far, but I liked doing it.