defpred S₁[ 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₁[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₁[x,y] ) by A1;
hence ( i <= j iff i9 <= j9 ) by A2, A3, ORDERS_2:def 5; :: thesis: verum