let i, j be Element of (inf_net N); :: according to WAYBEL11:def 9 :: thesis: ( not i <= j or (inf_net N) . i <= (inf_net N) . j )
assume A1: i <= j ; :: thesis: (inf_net N) . i <= (inf_net N) . j
consider f being Function of N,R such that
A2: ( inf_net N = N *' f & ( for i being Element of N holds f . i = "/\" { (N . k) where k is Element of N : k >= i } ,R ) ) by Def4;
A3: RelStr(# the carrier of (inf_net N),the InternalRel of (inf_net N) #) = RelStr(# the carrier of N,the InternalRel of N #) by A2, Def3;
then reconsider i' = i, j' = j as Element of N ;
deffunc H₁( Element of N) -> Element of the carrier of R = N . R;
defpred S₁[ Element of N] means R >= j';
defpred S₂[ Element of N] means R >= i';
set J = { H₁(k) where k is Element of N : S₁[k] } ;
set I = { H₁(k) where k is Element of N : S₂[k] } ;
A4: { H₁(k) where k is Element of N : S₁[k] } is Subset of R from DOMAIN_1:sch 8();
consider j0 being Element of N such that
A5: ( j0 >= j' & j0 >= j' ) by YELLOW_6:def 5;
N . j0 in { H₁(k) where k is Element of N : S₁[k] } by A5;
then reconsider J' = { H₁(k) where k is Element of N : S₁[k] } as non empty Subset of R by A4;
A6: { H₁(k) where k is Element of N : S₂[k] } is Subset of R from DOMAIN_1:sch 8();
consider j1 being Element of N such that
A7: ( j1 >= i' & j1 >= i' ) by YELLOW_6:def 5;
N . j1 in { H₁(k) where k is Element of N : S₂[k] } by A7;
then reconsider I' = { H₁(k) where k is Element of N : S₂[k] } as non empty Subset of R by A6;
A8: ( ex_inf_of J',R & ex_inf_of I',R ) by WAYBEL_0:76;
A9: J' c= I'

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in J' or a in I' )
assume A10: a in J' ; :: thesis: a in I'
then reconsider x = a as Element of R ;
consider k being Element of N such that
A11: x = N . k and
A12: k >= j' by A10;
reconsider k' = k as Element of N ;
( i' <= j' & j' <= k' ) by A1, A3, A12, YELLOW_0:1;
then i' <= k' by YELLOW_0:def 2;
hence a in I' by A11; :: thesis: verum

end;

A13: ( f . i' = "/\" { H₁(k) where k is Element of N : S₂[k] } ,R & f . j' = "/\" { H₁(k) where k is Element of N : S₁[k] } ,R ) by A2;
the mapping of (inf_net N) = f by A2, Def3;
hence (inf_net N) . i <= (inf_net N) . j by A8, A9, A13, YELLOW_0:35; :: thesis: verum