let A be domRing; :: thesis: ( Non_ZeroDiv_Set A = ([#] A) \ {(0. A)} & Non_ZeroDiv_Set A is non empty multiplicatively-closed without_zero Subset of A )
A1: Non_ZeroDiv_Set A = ([#] A) \ {(0. A)} by Th4;
( 0. A in [#] A & 0. A in {(0. A)} ) by TARSKI:def 1;
then Non_ZeroDiv_Set A is without_zero by A1, XBOOLE_0:def 5;
hence ( Non_ZeroDiv_Set A = ([#] A) \ {(0. A)} & Non_ZeroDiv_Set A is non empty multiplicatively-closed without_zero Subset of A ) by Th4; :: thesis: verum