negació de desigualtat

Sigui A totalment ordenat.

¬( x [< y ) <==> y < x

[<==] absurd

x [< y & ( y [< x & y != x )

[==>]

( x [< y || y [< x ) & ¬( x [< y)

y [< x & ¬( x [< y )

y [< x & ( ¬( x [< y ) || ¬( y [< x ) )

y [< x & y != x