thus ( A is transitive implies for x, y, z being Element of A st x <= y & y <= z holds
x <= z ) by ORDERS_2:26; :: thesis: ( ( for x, y, z being Element of A st x <= y & y <= z holds
x <= z ) implies A is transitive )
assume A1: for x, y, z being Element of A st x <= y & y <= z holds
x <= z ; :: thesis: A is transitive
let x, y, z be set ; :: according to RELAT_2:def 8,ORDERS_2:def 5 :: thesis: ( not x in the carrier of A or not y in the carrier of A or not z in the carrier of A or not [x,y] in the InternalRel of A or not [y,z] in the InternalRel of A or [x,z] in the InternalRel of A )
assume A2: ( x in the carrier of A & y in the carrier of A & z in the carrier of A ) ; :: thesis: ( not [x,y] in the InternalRel of A or not [y,z] in the InternalRel of A or [x,z] in the InternalRel of A )
assume A3: ( [x,y] in the InternalRel of A & [y,z] in the InternalRel of A ) ; :: thesis: [x,z] in the InternalRel of A
reconsider x = x, y = y, z = z as Element of A by A2;
( x <= y & y <= z ) by A3, ORDERS_2:def 9;
then x <= z by A1;
hence [x,z] in the InternalRel of A by ORDERS_2:def 9; :: thesis: verum