thus ( A is antisymmetric implies for x, y being Element of A st x <= y & y <= x holds
x = y ) by ORDERS_2:2; :: thesis: ( ( for x, y being Element of A st x <= y & y <= x holds
x = y ) implies A is antisymmetric )
assume A4: for x, y being Element of A st x <= y & y <= x holds
x = y ; :: thesis: A is antisymmetric
let x, y be object ; :: according to RELAT_2:def 4,ORDERS_2:def 4 :: thesis: ( not x in the carrier of A or not y in the carrier of A or not [x,y] in the InternalRel of A or not [y,x] in the InternalRel of A or x = y )
assume A5: ( x in the carrier of A & y in the carrier of A ) ; :: thesis: ( not [x,y] in the InternalRel of A or not [y,x] in the InternalRel of A or x = y )
assume A6: ( [x,y] in the InternalRel of A & [y,x] in the InternalRel of A ) ; :: thesis: x = y
reconsider x = x, y = y as Element of A by A5;
( x <= y & y <= x ) by A6;
hence x = y by A4; :: thesis: verum