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 i9, j9 being Element of NAT st i9 = i & j9 = i9 + 1 & j9 = 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 i9, j9 being Element of NAT st i9 = i & j9 = i9 + 1 & j9 = 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 i9, j9 being Element of NAT st i9 = i & j9 = i9 + 1 & j9 = 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 i9, j9 be Element of NAT ; :: thesis: ( i9 = i & j9 = i9 + 1 & j9 = 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 that
A1: i9 = i and
A2: j9 = i9 + 1 and
A3: j9 = 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 A4: 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 S1[ 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 A5: (Net-Str (a,b)) . i = a ; :: thesis: (Net-Str (a,b)) . j = b
S1[i9]
proof
assume A6: not S1[i9] ; :: thesis: contradiction
(Net-Str (a,b)) . i = ((a,b) ,...) . i by Def3
.= b by A1, A6, Def1 ;
hence contradiction by A4, A5; :: thesis: verum
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: verum
end;
assume A8: (Net-Str (a,b)) . i = b ; :: thesis: (Net-Str (a,b)) . j = a
A9: not S1[i9]
proof
assume A10: S1[i9] ; :: thesis: contradiction
(Net-Str (a,b)) . i = ((a,b) ,...) . i by Def3
.= a by ;
hence contradiction by A4, A8; :: thesis: verum
end;
A11: S1[j9] (Net-Str (a,b)) . j = ((a,b) ,...) . j by Def3
.= a by ;
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;