let S be non empty RelStr ; :: thesis:
let a, b be Element of ; :: thesis:
let i, j be Element of ; :: thesis:
let i', j' be Element of NAT ; :: thesis:
assume that
A1: i' = i and
A2: j' = i' + 1 and
A3: j' = 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₁[i']

proof

assume A6: not S₁[i'] ; :: 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 j' <> 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₁[i']

proof

assume A10: S₁[i'] ; :: 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₁[j']

proof

assume not S₁[j'] ; :: thesis:
then ex kl being Element of NAT st j' = (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;