defpred S_{1}[ 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 S_{1}[x,y] )
from RELSET_1:sch 2();

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 S_{1}[x,y] )
by A1;

hence ( i <= j iff i9 <= j9 ) by A2, A3, ORDERS_2:def 5; :: thesis: verum

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 S

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 S

hence ( i <= j iff i9 <= j9 ) by A2, A3, ORDERS_2:def 5; :: thesis: verum