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	$$⊢\mathrm{LB}R=\mathrm{UB}{R}^{-1}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1	0	clb	$$class\mathrm{LB}R$$
2	0	ccnv	$$class{R}^{-1}$$
3	2	cub	$$class\mathrm{UB}{R}^{-1}$$
4	1 3	wceq	$$wff\mathrm{LB}R=\mathrm{UB}{R}^{-1}$$