set L = Net-Str (a,b);
thus
Net-Str (a,b) is reflexive
( Net-Str (a,b) is transitive & Net-Str (a,b) is directed & Net-Str (a,b) is antisymmetric )
thus
Net-Str (a,b) is transitive
( Net-Str (a,b) is directed & Net-Str (a,b) is antisymmetric )
[#] (Net-Str (a,b)) is directed
proof
let x,
y be
Element of
(Net-Str (a,b));
WAYBEL_0:def 1 ( 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))
;
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
;
( 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;
verum
end;
hence
Net-Str (a,b) is directed
; Net-Str (a,b) is antisymmetric
thus
Net-Str (a,b) is antisymmetric
verum