set L = Net-Str a,b;
thus Net-Str a,b is reflexive :: thesis: ( Net-Str a,b is transitive & Net-Str a,b is directed & Net-Str a,b is antisymmetric )

proof

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

end;

thus Net-Str a,b is transitive :: thesis: ( Net-Str a,b is directed & Net-Str a,b is antisymmetric )

proof

let x, y, z be Element of (Net-Str a,b); :: according to YELLOW_0:def 2 :: thesis: ( not x <= y or not y <= z or x <= z )
assume that
A1: x <= y and
A2: y <= z ; :: thesis: x <= z
reconsider x9 = x, y9 = y, z9 = z as Element of NAT by Def3;
A3: x9 <= y9 by A1, Def3;
y9 <= z9 by A2, Def3;
then x9 <= z9 by A3, XXREAL_0:2;
hence x <= z by Def3; :: thesis: verum

end;

[#] (Net-Str a,b) is directed

proof

let x, y be Element of (Net-Str a,b); :: according to WAYBEL_0:def 1 :: thesis: ( not x in [#] (Net-Str a,b) or not y in [#] (Net-Str a,b) or ex b₁ being Element of the carrier of (Net-Str a,b) st
( b₁ in [#] (Net-Str a,b) & x <= b₁ & y <= b₁ ) )
assume that
x in [#] (Net-Str a,b) and
y in [#] (Net-Str a,b) ; :: thesis: ex b₁ being Element of the carrier of (Net-Str a,b) st
( b₁ in [#] (Net-Str a,b) & x <= b₁ & y <= b₁ )
reconsider x9 = x, y9 = y as Element of NAT by Def3;
set z9 = x9 + y9;
reconsider z = x9 + y9 as Element of (Net-Str a,b) by Def3;
reconsider z = z as Element of (Net-Str a,b) ;
take z ; :: thesis: ( z in [#] (Net-Str a,b) & x <= z & y <= z )
A4: x9 <= x9 + y9 by NAT_1:11;
y9 <= x9 + y9 by NAT_1:11;
hence ( z in [#] (Net-Str a,b) & x <= z & y <= z ) by A4, Def3; :: thesis: verum

end;

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

proof

let x, y be Element of (Net-Str a,b); :: according to YELLOW_0:def 3 :: thesis: ( not x <= y or not y <= x or x = y )
reconsider x9 = x, y9 = y as Element of NAT by Def3;
assume that
A5: x <= y and
A6: y <= x ; :: thesis: x = y
A7: x9 <= y9 by A5, Def3;
y9 <= x9 by A6, Def3;
hence x = y by A7, XXREAL_0:1; :: thesis: verum

end;