reconsider M = {(1. A)} as non empty multiplicatively-closed Subset of A by Th5;
take M ; :: thesis: M is without_zero
thus M is without_zero by TARSKI:def 1; :: thesis: verum