Theorem ltnsym

Description: 'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002)

	Ref	Expression
Assertion	ltnsym	|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> -. B < A ) )

Proof

Step	Hyp	Ref	Expression
1		axlttri	|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> -. ( A = B \/ B < A ) ) )
2		pm2.46	|- ( -. ( A = B \/ B < A ) -> -. B < A )
3	1 2	biimtrdi	|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> -. B < A ) )