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⊥ ⊥

Syntax hints:   ≤ wle 2  ^⊥ wn 4

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

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

This theorem is referenced by: (None)