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 b1 being Element of S holds b1 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 b1 being Element of S holds b1 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;