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 )

thus Net-Str (a,b) is antisymmetric :: thesis: verum

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

thus
Net-Str (a,b) is transitive
:: thesis: ( Net-Str (a,b) is directed & Net-Str (a,b) is antisymmetric )
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;reconsider x9 = x as Element of NAT by Def3;

x9 <= x9 ;

hence x <= x by Def3; :: thesis: verum

proof

[#] (Net-Str (a,b)) is directed
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;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

proof

hence
Net-Str (a,b) is directed
; :: thesis: Net-Str (a,b) is antisymmetric
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_{1} being Element of the carrier of (Net-Str (a,b)) st

( b_{1} in [#] (Net-Str (a,b)) & x <= b_{1} & y <= b_{1} ) )

assume that

x in [#] (Net-Str (a,b)) and

y in [#] (Net-Str (a,b)) ; :: thesis: ex b_{1} being Element of the carrier of (Net-Str (a,b)) st

( b_{1} in [#] (Net-Str (a,b)) & x <= b_{1} & y <= b_{1} )

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;( b

assume that

x in [#] (Net-Str (a,b)) and

y in [#] (Net-Str (a,b)) ; :: thesis: ex b

( 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

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;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