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 ;
y9 <= z9 by ;
then x9 <= z9 by ;
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 b1 being Element of the carrier of (Net-Str (a,b)) st
( b1 in [#] (Net-Str (a,b)) & x <= b1 & y <= b1 ) )

assume that
x in [#] (Net-Str (a,b)) and
y in [#] (Net-Str (a,b)) ; :: thesis: ex b1 being Element of the carrier of (Net-Str (a,b)) st
( b1 in [#] (Net-Str (a,b)) & x <= b1 & y <= b1 )

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 ; :: thesis: verum
end;
hence Net-Str (a,b) is directed ; :: 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 ;
y9 <= x9 by ;
hence x = y by ; :: thesis: verum
end;