let a, b be Element of R; :: thesis: ( R42(R,a,b) implies not R42(R,b,a) )
assume [a,b] in the InternalRel of R ; :: according to ORDERS_2:def 5 :: thesis: R42(R,b,a)
hence not [b,a] in the InternalRel of R by PREFER_1:22; :: according to ORDERS_2:def 5 :: thesis: verum