0 in StoppingSet T ;
hence not StoppingSet T is empty ; :: thesis: verum