0. S <> 1. S by Def8;
hence not 1. S is zero by Def12; :: thesis: verum