consider x, y being Element of S such that

A1: x <> y by Def10;

A1: x <> y by Def10;

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

end;

suppose A2:
x <> 0. S
; :: thesis: not for b_{1} being Element of S holds b_{1} is zero

take
x
; :: thesis: not x is zero

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

end;thus x <> 0. S by A2; :: according to STRUCT_0:def 12 :: thesis: verum

suppose A3:
y <> 0. S
; :: thesis: not for b_{1} being Element of S holds b_{1} is zero

take
y
; :: thesis: not y is zero

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

end;thus y <> 0. S by A3; :: according to STRUCT_0:def 12 :: thesis: verum