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 ) )

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 )
;

end;

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 S_{1}[ 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 )

A9: not S_{1}[i9]
_{1}[j9]

.= a by A3, A11, Def1 ;

hence (Net-Str (a,b)) . j = a ; :: thesis: verum

end;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 A8:
(Net-Str (a,b)) . i = b
; :: thesis: (Net-Str (a,b)) . j = a
assume A5:
(Net-Str (a,b)) . i = a
; :: thesis: (Net-Str (a,b)) . j = b

S_{1}[i9]

(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;S

proof

then A7:
for k being Element of NAT holds j9 <> 2 * k
by A2;
assume A6:
not S_{1}[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;(Net-Str (a,b)) . i = ((a,b) ,...) . i by Def3

.= b by A1, A6, Def1 ;

hence contradiction by A4, A5; :: thesis: verum

(Net-Str (a,b)) . j = ((a,b) ,...) . j by Def3

.= b by A3, A7, Def1 ;

hence (Net-Str (a,b)) . j = b ; :: thesis: verum

A9: not S

proof

A11:
S
assume A10:
S_{1}[i9]
; :: thesis: contradiction

(Net-Str (a,b)) . i = ((a,b) ,...) . i by Def3

.= a by A1, A10, Def1 ;

hence contradiction by A4, A8; :: thesis: verum

end;(Net-Str (a,b)) . i = ((a,b) ,...) . i by Def3

.= a by A1, A10, Def1 ;

hence contradiction by A4, A8; :: thesis: verum

proof

(Net-Str (a,b)) . j =
((a,b) ,...) . j
by Def3
assume
not S_{1}[j9]
; :: thesis: contradiction

then ex kl being Element of NAT st j9 = (2 * kl) + 1 by SCHEME1:1;

hence contradiction by A2, A9; :: thesis: verum

end;then ex kl being Element of NAT st j9 = (2 * kl) + 1 by SCHEME1:1;

hence contradiction by A2, A9; :: thesis: verum

.= a by A3, A11, Def1 ;

hence (Net-Str (a,b)) . j = a ; :: thesis: verum

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;