let S be non empty RelStr ; :: thesis: for a, b being Element of S

for i being Element of (Net-Str (a,b)) holds

( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b )

let a, b be Element of S; :: thesis: for i being Element of (Net-Str (a,b)) holds

( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b )

let i be Element of (Net-Str (a,b)); :: thesis: ( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b )

set N = Net-Str (a,b);

reconsider I = i as Element of NAT by Def3;

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

defpred S_{1}[ Element of NAT ] means ex k being Element of NAT st $1 = 2 * k;

for i being Element of (Net-Str (a,b)) holds

( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b )

let a, b be Element of S; :: thesis: for i being Element of (Net-Str (a,b)) holds

( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b )

let i be Element of (Net-Str (a,b)); :: thesis: ( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b )

set N = Net-Str (a,b);

reconsider I = i as Element of NAT by Def3;

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

defpred S

per cases
( S_{1}[I] or not S_{1}[I] )
;

end;