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;