set L = Net-Str a,b;
thus Net-Str a,b is reflexive :: thesis:

let x be Element of (Net-Str a,b); :: according to YELLOW_0:def 1 :: thesis:
reconsider x' = x as Element of NAT by Def3;
x' <= x' ;
hence x <= x by Def3; :: thesis:

end;

thus Net-Str a,b is transitive :: thesis:

let x, y, z be Element of (Net-Str a,b); :: according to YELLOW_0:def 2 :: thesis:
assume A1: ( x <= y & y <= z ) ; :: thesis:
reconsider x' = x, y' = y, z' = z as Element of NAT by Def3;
( x' <= y' & y' <= z' ) by A1, Def3;
then x' <= z' by XXREAL_0:2;
hence x <= z by Def3; :: thesis:

end;

thus Net-Str a,b is directed :: thesis:

let x, y be Element of (Net-Str a,b); :: according to WAYBEL_0:def 1 :: thesis:
assume ( x in [#] (Net-Str a,b) & y in [#] (Net-Str a,b) ) ; :: thesis:
reconsider x' = x, y' = y as Element of NAT by Def3;
set z' = x' + y';
reconsider z = x' + y' as Element of (Net-Str a,b) by Def3;
reconsider z = z as Element of (Net-Str a,b) ;
take z ; :: thesis:
( z in the carrier of (Net-Str a,b) & x' <= x' + y' & y' <= x' + y' ) by NAT_1:11;
hence ( z in [#] (Net-Str a,b) & x <= z & y <= z ) by Def3; :: thesis:

end;

hence Net-Str a,b is directed by WAYBEL_0:def 6; :: thesis:

end;

thus Net-Str a,b is antisymmetric :: thesis:

let x, y be Element of (Net-Str a,b); :: according to YELLOW_0:def 3 :: thesis:
reconsider x' = x, y' = y as Element of NAT by Def3;
assume ( x <= y & y <= x ) ; :: thesis:
then ( x' <= y' & y' <= x' ) by Def3;
hence x = y by XXREAL_0:1; :: thesis:

end;