Definition df-lb

Description: Define the lower bound relationship functor. See brlb for value. (Contributed by Scott Fenton, 3-May-2018)

	Ref	Expression
Assertion	df-lb	⊢ LB 𝑅 = UB ◡ 𝑅

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1	0	clb	⊢ LB 𝑅
2	0	ccnv	⊢ ◡ 𝑅
3	2	cub	⊢ UB ◡ 𝑅
4	1 3	wceq	⊢ LB 𝑅 = UB ◡ 𝑅