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 x9 = x as Element of NAT by Def3;
x9 <= x9 ;
hence x <= x by Def3; :: thesis:

end;

let x, y, z be Element of (Net-Str (a,b)); :: according to YELLOW_0:def 2 :: thesis:
assume that
A1: x <= y and
A2: y <= z ; :: thesis:
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:

end;

let x, y be Element of (Net-Str (a,b)); :: according to WAYBEL_0:def 1 :: thesis:
assume that
x in [#] (Net-Str (a,b)) and
y in [#] (Net-Str (a,b)) ; :: thesis:
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:
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:

end;

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

end;