consider x, y being Element of S such that
A1: x <> y by Def10;

per cases ( x <> 0. S or y <> 0. S ) by A1;

suppose A2: x <> 0. S ; :: thesis: not for b₁ being Element of S holds b₁ is zero

take x ; :: thesis: not x is zero
thus x <> 0. S by A2; :: according to STRUCT_0:def 12 :: thesis: verum

end;

suppose A3: y <> 0. S ; :: thesis: not for b₁ being Element of S holds b₁ is zero

take y ; :: thesis: not y is zero
thus y <> 0. S by A3; :: according to STRUCT_0:def 12 :: thesis: verum

end;

end;