defpred S1[ set , set ] means for i, j being Element of NAT st i = \$1 & j = \$2 holds
i <= j;
consider R being Relation of NAT,NAT such that
A1: for x, y being Element of NAT holds
( [x,y] in R iff S1[x,y] ) from reconsider R = R as Relation of NAT ;
take N = NetStr(# NAT,R,((a,b) ,...) #); :: thesis: ( the carrier of N = NAT & the mapping of N = (a,b) ,... & ( for i, j being Element of N
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ) )

thus the carrier of N = NAT ; :: thesis: ( the mapping of N = (a,b) ,... & ( for i, j being Element of N
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ) )

thus the mapping of N = (a,b) ,... ; :: thesis: for i, j being Element of N
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 )

let i, j be Element of N; :: thesis: for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 )

let i9, j9 be Element of NAT ; :: thesis: ( i = i9 & j = j9 implies ( i <= j iff i9 <= j9 ) )
assume that
A2: i = i9 and
A3: j = j9 ; :: thesis: ( i <= j iff i9 <= j9 )
reconsider x = i, y = j as Element of NAT ;
( [x,y] in the InternalRel of N iff S1[x,y] ) by A1;
hence ( i <= j iff i9 <= j9 ) by ; :: thesis: verum