let S be non empty RelStr ; :: thesis: for a, b being Element of S
for i, j being Element of (Net-Str a,b)
for i', j' being Element of NAT st i' = i & j' = i' + 1 & j' = j holds
( ( (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 ) )
let a, b be Element of S; :: thesis: for i, j being Element of (Net-Str a,b)
for i', j' being Element of NAT st i' = i & j' = i' + 1 & j' = j holds
( ( (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 ) )
let i, j be Element of (Net-Str a,b); :: thesis: for i', j' being Element of NAT st i' = i & j' = i' + 1 & j' = j holds
( ( (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 ) )
let i', j' be Element of NAT ; :: thesis: ( i' = i & j' = i' + 1 & j' = j implies ( ( (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 ) ) )
assume A1: ( i' = i & j' = i' + 1 & j' = j ) ; :: thesis: ( ( (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 ) )

per cases ( a <> b or a = b ) ;

suppose A2: a <> b ; :: thesis: ( ( (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 ) )

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: ( (Net-Str a,b) . i = b implies (Net-Str a,b) . j = a )

proof

assume A3: (Net-Str a,b) . i = a ; :: thesis: (Net-Str a,b) . j = b
S₁[i']

proof

assume A4: not S₁[i'] ; :: thesis: contradiction
(Net-Str a,b) . i = (a,b ,... ) . i by Def3
.= b by A1, A4, Def1 ;
hence contradiction by A2, A3; :: thesis: verum

end;

then consider k being Element of NAT such that
A5: i' = 2 * k ;
A6: for k being Element of NAT holds j' <> 2 * k by A1, A5;
(Net-Str a,b) . j = (a,b ,... ) . j by Def3
.= b by A1, A6, Def1 ;
hence (Net-Str a,b) . j = b ; :: thesis: verum

end;

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

proof

assume A9: S₁[i'] ; :: thesis: contradiction
(Net-Str a,b) . i = (a,b ,... ) . i by Def3
.= a by A1, A9, Def1 ;
hence contradiction by A2, A7; :: thesis: verum

end;

A10: S₁[j']

proof

assume not S₁[j'] ; :: thesis: contradiction
then consider kl being Element of NAT such that
A11: j' = (2 * kl) + 1 by SCHEME1:1;
thus contradiction by A1, A8, A11; :: thesis: verum

end;

(Net-Str a,b) . j = (a,b ,... ) . j by Def3
.= a by A1, A10, Def1 ;
hence (Net-Str a,b) . j = a ; :: thesis: verum

end;

suppose a = b ; :: thesis: ( ( (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 ) )

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: verum

end;

end;