let S be non empty RelStr ; :: thesis:
let a, b be Element of S; :: thesis:
let i, j be Element of (Net-Str (a,b)); :: thesis:
let i9, j9 be Element of NAT ; :: thesis:
assume that
A1: i9 = i and
A2: j9 = i9 + 1 and
A3: j9 = j ; :: thesis:

per cases ;

suppose A4: a <> b ; :: thesis:

defpred S₁[ Element of NAT ] means ex k being Element of NAT st $1 = 2 * k;
thus ( (Net-Str (a,b)) . i = a implies (Net-Str (a,b)) . j = b ) :: thesis:

proof

assume A5: (Net-Str (a,b)) . i = a ; :: thesis:
S₁[i9]

proof

assume A6: not S₁[i9] ; :: thesis:
(Net-Str (a,b)) . i = ((a,b) ,...) . i by Def3
.= b by A1, A6, Def1 ;
hence contradiction by A4, A5; :: thesis:

end;

then A7: for k being Element of NAT holds j9 <> 2 * k by A2;
(Net-Str (a,b)) . j = ((a,b) ,...) . j by Def3
.= b by A3, A7, Def1 ;
hence (Net-Str (a,b)) . j = b ; :: thesis:

end;

assume A8: (Net-Str (a,b)) . i = b ; :: thesis:
A9: not S₁[i9]

proof

assume A10: S₁[i9] ; :: thesis:
(Net-Str (a,b)) . i = ((a,b) ,...) . i by Def3
.= a by A1, A10, Def1 ;
hence contradiction by A4, A8; :: thesis:

end;

A11: S₁[j9]

proof

assume not S₁[j9] ; :: thesis:
then ex kl being Element of NAT st j9 = (2 * kl) + 1 by SCHEME1:1;
hence contradiction by A2, A9; :: thesis:

end;

(Net-Str (a,b)) . j = ((a,b) ,...) . j by Def3
.= a by A3, A11, Def1 ;
hence (Net-Str (a,b)) . j = a ; :: thesis:

end;

suppose a = b ; :: thesis:

hence ( ( (Net-Str (a,b)) . i = a implies (Net-Str (a,b)) . j = b ) & ( (Net-Str (a,b)) . i = b implies (Net-Str (a,b)) . j = a ) ) by Th5; :: thesis:

end;

end;