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 , 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 ;
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
for i', j' being Element of NAT st i = i' & j = j' holds
( i <= j iff i' <= j' ) ) )
thus the carrier of N = NAT ; :: thesis: ( the mapping of N = a,b ,... & ( for i, j being Element of
for i', j' being Element of NAT st i = i' & j = j' holds
( i <= j iff i' <= j' ) ) )
thus the mapping of N = a,b ,... ; :: thesis: for i, j being Element of
for i', j' being Element of NAT st i = i' & j = j' holds
( i <= j iff i' <= j' )
let i, j be Element of ; :: thesis: for i', j' being Element of NAT st i = i' & j = j' holds
( i <= j iff i' <= j' )
let i', j' be Element of NAT ; :: thesis: ( i = i' & j = j' implies ( i <= j iff i' <= j' ) )
assume that
A2: i = i' and
A3: j = j' ; :: thesis: ( i <= j iff i' <= j' )
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 i' <= j' ) by A2, A3, ORDERS_2:def 9; :: thesis: verum