df-one - Linear Logic Proof Explorer

	Linear Logic Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > LLPE Home > Th. List > df-one		Structured version

Definition df-one 104

Description: One is the dual of Bottom.

**Assertion**
Ref	Expression
df-one	⊦ (1 ⧟ ~ ⊥)

**Detailed syntax breakdown of Definition df-one**
Step	Hyp	Ref	Expression
1		wone 103	. 2 wff 1
2		wbot 1	. . 3 wff ⊥
3	2	wneg 3	. 2 wff ~ ⊥
4	1, 3	wlb 55	1 wff (1 ⧟ ~ ⊥)

Colors of variables: wff var nilad

This definition is referenced by: (None)