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)

for x being object st x in the carrier of (a_net F) holds

[x,x] in the InternalRel of (a_net F)

hence ( a_net F is reflexive & a_net F is transitive ) by A7, ORDERS_2:def 2, ORDERS_2:def 3; :: thesis: verum

[x,z] in the InternalRel of (a_net F)

proof

then A7:
the InternalRel of (a_net F) is_transitive_in the carrier of (a_net F)
by RELAT_2:def 8;
let x, y, z be object ; :: thesis: ( 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) ; :: thesis: [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; :: thesis: verum

end;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) ; :: thesis: [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; :: thesis: verum

for x being object st x in the carrier of (a_net F) holds

[x,x] in the InternalRel of (a_net F)

proof

then
the InternalRel of (a_net F) is_reflexive_in the carrier of (a_net F)
by RELAT_2:def 1;
let x be object ; :: thesis: ( x in the carrier of (a_net F) implies [x,x] in the InternalRel of (a_net F) )

assume x in the carrier of (a_net F) ; :: thesis: [x,x] in the InternalRel of (a_net F)

then reconsider i = x as Element of (a_net F) ;

i `2 c= i `2 ;

then i <= i by Def4;

hence [x,x] in the InternalRel of (a_net F) by ORDERS_2:def 5; :: thesis: verum

end;assume x in the carrier of (a_net F) ; :: thesis: [x,x] in the InternalRel of (a_net F)

then reconsider i = x as Element of (a_net F) ;

i `2 c= i `2 ;

then i <= i by Def4;

hence [x,x] in the InternalRel of (a_net F) by ORDERS_2:def 5; :: thesis: verum

hence ( a_net F is reflexive & a_net F is transitive ) by A7, ORDERS_2:def 2, ORDERS_2:def 3; :: thesis: verum