set M = ([#] A) \ (ZeroDiv_Set A);
A1: not 1. A in ZeroDiv_Set A

proof

assume 1. A in ZeroDiv_Set A ; :: thesis: contradiction
then consider a being Element of [#] A such that
A2: a = 1. A and
A3: a is Zero_Divisor of A ;
thus contradiction by Th2, A2, A3; :: thesis: verum

end;

for v, u being Element of A st v in ([#] A) \ (ZeroDiv_Set A) & u in ([#] A) \ (ZeroDiv_Set A) holds
v * u in ([#] A) \ (ZeroDiv_Set A)

proof

let v, u be Element of A; :: thesis: ( v in ([#] A) \ (ZeroDiv_Set A) & u in ([#] A) \ (ZeroDiv_Set A) implies v * u in ([#] A) \ (ZeroDiv_Set A) )
assume A5: ( v in ([#] A) \ (ZeroDiv_Set A) & u in ([#] A) \ (ZeroDiv_Set A) ) ; :: thesis: v * u in ([#] A) \ (ZeroDiv_Set A)
assume not v * u in ([#] A) \ (ZeroDiv_Set A) ; :: thesis: contradiction
then v * u in ZeroDiv_Set A by XBOOLE_0:def 5;
then consider w being Element of [#] A such that
A7: w = v * u and
A8: w is Zero_Divisor of A ;
w is zero_divisible by A8;
then consider b being Element of A such that
A9: b <> 0. A and
A10: w * b = 0. A ;
A11: v * (u * b) = 0. A by A10, A7, GROUP_1:def 3;

per cases ( u * b <> 0. A or u * b = 0. A ) ;

suppose u * b <> 0. A ; :: thesis: contradiction

then v is zero_divisible by A11;
then v in ZeroDiv_Set A ;
hence contradiction by A5, XBOOLE_0:def 5; :: thesis: verum

end;

suppose u * b = 0. A ; :: thesis: contradiction

then u is zero_divisible by A9;
then u in ZeroDiv_Set A ;
hence contradiction by A5, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

hence Non_ZeroDiv_Set A is multiplicatively-closed by A1, XBOOLE_0:def 5; :: thesis: verum