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 5; :: 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 that
x <= y and
y <= z ; :: thesis: x <= z
A2: x = e by Th25;
z = e by Th25;
hence x <= z by A1, A2, ORDERS_2:def 5; :: 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 3 :: thesis: ex b₁ being Element of the carrier of (Net-Str e) st
( x <= b₁ & y <= b₁ )
take e ; :: thesis: ( x <= e & y <= e )
A3: x = e by Th25;
y = e by Th25;
hence ( x <= e & y <= e ) by A1, A3, ORDERS_2:def 5; :: 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 that
x <= y and
y <= x ; :: thesis: x = y
x = e by Th25;
hence x = y by Th25; :: thesis: verum