Description: A Hilbert lattice has the superposition property. Theorem 13.2 in Crawley p. 107. (Contributed by NM, 30-Jan-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hlsupr.l | |
|
hlsupr.j | |
||
hlsupr.a | |
||
Assertion | hlsupr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlsupr.l | |
|
2 | hlsupr.j | |
|
3 | hlsupr.a | |
|
4 | eqid | |
|
5 | 4 1 2 3 | hlsuprexch | |
6 | 5 | simpld | |
7 | 6 | imp | |