0 c= alpha ;
then ConwayDay 0 c= ConwayDay alpha by Th3;
hence not ConwayDay alpha is empty by Th2; :: thesis: verum