for x, y, z being object st x in the carrier of (a_net F) & y in the carrier of (a_net F) & z in the carrier of (a_net F) & [x,y] in the InternalRel of (a_net F) & [y,z] in the InternalRel of (a_net F) holds
[x,z] in the InternalRel of (a_net F)
proof
let x,
y,
z be
object ;
( x in the carrier of (a_net F) & y in the carrier of (a_net F) & z in the carrier of (a_net F) & [x,y] in the InternalRel of (a_net F) & [y,z] in the InternalRel of (a_net F) implies [x,z] in the InternalRel of (a_net F) )
assume that A1:
x in the
carrier of
(a_net F)
and A2:
y in the
carrier of
(a_net F)
and A3:
z in the
carrier of
(a_net F)
and A4:
[x,y] in the
InternalRel of
(a_net F)
and A5:
[y,z] in the
InternalRel of
(a_net F)
;
[x,z] in the InternalRel of (a_net F)
reconsider k =
z as
Element of
(a_net F) by A3;
reconsider j =
y as
Element of
(a_net F) by A2;
j <= k
by A5, ORDERS_2:def 5;
then A6:
k `2 c= j `2
by Def4;
reconsider i =
x as
Element of
(a_net F) by A1;
i <= j
by A4, ORDERS_2:def 5;
then
j `2 c= i `2
by Def4;
then
k `2 c= i `2
by A6;
then
i <= k
by Def4;
hence
[x,z] in the
InternalRel of
(a_net F)
by ORDERS_2:def 5;
verum
end;
then A7:
the InternalRel of (a_net F) is_transitive_in the carrier of (a_net F)
by RELAT_2:def 8;
for x being object st x in the carrier of (a_net F) holds
[x,x] in the InternalRel of (a_net F)
then
the InternalRel of (a_net F) is_reflexive_in the carrier of (a_net F)
by RELAT_2:def 1;
hence
( a_net F is reflexive & a_net F is transitive )
by A7, ORDERS_2:def 2, ORDERS_2:def 3; verum