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₁[ Element of NAT ] means ex k being Element of NAT st $1 = 2 * k;

per cases ( S₁[I] or not S₁[I] ) ;

suppose S₁[I] ; :: thesis: ( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b )

hence ( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b ) by A1, Def1; :: thesis: verum

end;

suppose not S₁[I] ; :: thesis: ( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b )

hence ( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b ) by A1, Def1; :: thesis: verum

end;

end;