defpred S₁[ Element of S, Element of S] means f . $1 <= f . $2;
consider R being Relation of S,S such that
A1: for x, y being Element of S holds
( [x,y] in R iff S₁[x,y] ) from RELSET_1:sch 2();
take N = NetStr(# S,R,f #); :: thesis: ( the carrier of N = S & the mapping of N = f & ( for i, j being Element of N holds
( i <= j iff N . i <= N . j ) ) )
thus the carrier of N = S ; :: thesis: ( the mapping of N = f & ( for i, j being Element of N holds
( i <= j iff N . i <= N . j ) ) )
thus the mapping of N = f ; :: thesis: for i, j being Element of N holds
( i <= j iff N . i <= N . j )
let i, j be Element of N; :: thesis: ( i <= j iff N . i <= N . j )
reconsider x = i, y = j as Element of S ;
( [x,y] in the InternalRel of N iff f . x <= f . y ) by A1;
hence ( i <= j iff N . i <= N . j ) by ORDERS_2:def 5; :: thesis: verum