ADTS (Spectrum R) is empty by Def3;
hence ADTS (Spectrum R) is T_0 ; :: thesis: verum