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 and
A3: for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) by Def4;
A4: 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 i9 = i, j9 = 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 >= j9;
defpred S₂[ Element of N] means R >= i9;
set J = { H₁(k) where k is Element of N : S₁[k] } ;
set I = { H₁(k) where k is Element of N : S₂[k] } ;
A5: { 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
A6: j0 >= j9 and
j0 >= j9 by YELLOW_6:def 3;
N . j0 in { H₁(k) where k is Element of N : S₁[k] } by A6;
then reconsider J9 = { H₁(k) where k is Element of N : S₁[k] } as non empty Subset of R by A5;
A7: { 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
A8: j1 >= i9 and
j1 >= i9 by YELLOW_6:def 3;
N . j1 in { H₁(k) where k is Element of N : S₂[k] } by A8;
then reconsider I9 = { H₁(k) where k is Element of N : S₂[k] } as non empty Subset of R by A7;
A9: ex_inf_of J9,R by WAYBEL_0:76;
A10: ex_inf_of I9,R by WAYBEL_0:76;
A11: J9 c= I9

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in J9 or a in I9 )
assume A12: a in J9 ; :: thesis: a in I9
then reconsider x = a as Element of R ;
consider k being Element of N such that
A13: x = N . k and
A14: k >= j9 by A12;
reconsider k9 = k as Element of N ;
i9 <= j9 by A1, A4, YELLOW_0:1;
then i9 <= k9 by A14, YELLOW_0:def 2;
hence a in I9 by A13; :: thesis: verum

end;

A15: f . i9 = "/\" ( { H₁(k) where k is Element of N : S₂[k] } ,R) by A3;
A16: f . j9 = "/\" ( { H₁(k) where k is Element of N : S₁[k] } ,R) by A3;
the mapping of (inf_net N) = f by A2, Def3;
hence (inf_net N) . i <= (inf_net N) . j by A9, A10, A11, A15, A16, YELLOW_0:35; :: thesis: verum