Theorem gte-lteh

Description: Relationship between <_ and >_ using hypotheses. (Contributed by David A. Wheeler, 10-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	gte-lteh.1	|- A e. _V
	gte-lteh.2	|- B e. _V
Assertion	gte-lteh	|- ( A >_ B <-> B <_ A )

Proof

Step	Hyp	Ref	Expression
1		gte-lteh.1	|- A e. _V
2		gte-lteh.2	|- B e. _V
3		df-gte	|- >_ = `' <_
4	3	breqi	|- ( A >_ B <-> A `' <_ B )
5	1 2	brcnv	|- ( A `' <_ B <-> B <_ A )
6	4 5	bitri	|- ( A >_ B <-> B <_ A )