Theorem qlhoml1a 143

Description: An ortholattice inequality, corresponding to a theorem provable in Hilbert space. Part of Definition 2.1 p. 2092, in M. Pavicic and N. Megill, "Quantum and Classical Implicational Algebras with Primitive Implication", Int. J. of Theor. Phys. 37, 2091-2098 (1998). (Contributed by NM, 3-Feb-2002.)

Assertion

Ref	Expression
qlhoml1a	a ≤ a⊥ ⊥

Proof of Theorem qlhoml1a

Step	Hyp	Ref	Expression
1		ax-a1 30	. 2 a = a⊥ ⊥
2	1	bile 142	1 a ≤ a⊥ ⊥

This proof depends on syntax axioms:   ≤ wle 2  ^⊥ wn 4

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This proof depends on definitions:  df-t 41  df-f 42  df-le1 130

This theorem is used by: (None)