set N = Net-Str e;
the carrier of (Net-Str e) = {e} by Def11;
then reconsider e = e as Element of (Net-Str e) by TARSKI:def 1;
the InternalRel of (Net-Str e) = {[e,e]} by Def11;
then A1: [e,e] in the InternalRel of (Net-Str e) by TARSKI:def 1;
thus Net-Str e is reflexive :: thesis: ( Net-Str e is transitive & Net-Str e is directed & Net-Str e is antisymmetric )

proof

let x be Element of (Net-Str e); :: according to YELLOW_0:def 1 :: thesis: x <= x
x = e by Th25;
hence x <= x by A1, ORDERS_2:def 9; :: thesis: verum

end;

thus Net-Str e is transitive :: thesis: ( Net-Str e is directed & Net-Str e is antisymmetric )

proof

let x, y, z be Element of (Net-Str e); :: according to YELLOW_0:def 2 :: thesis: ( not x <= y or not y <= z or x <= z )
assume ( x <= y & y <= z ) ; :: thesis: x <= z
( x = e & z = e ) by Th25;
hence x <= z by A1, ORDERS_2:def 9; :: thesis: verum

end;

thus Net-Str e is directed :: thesis: Net-Str e is antisymmetric

proof

let x, y be Element of (Net-Str e); :: according to YELLOW_6:def 5 :: thesis: ex b₁ being Element of the carrier of (Net-Str e) st
( x <= b₁ & y <= b₁ )
take e ; :: thesis: ( x <= e & y <= e )
( x = e & y = e ) by Th25;
hence ( x <= e & y <= e ) by A1, ORDERS_2:def 9; :: thesis: verum

end;

let x, y be Element of (Net-Str e); :: according to YELLOW_0:def 3 :: thesis: ( not x <= y or not y <= x or x = y )
assume ( x <= y & y <= x ) ; :: thesis: x = y
( x = e & y = e ) by Th25;
hence x = y ; :: thesis: verum