Description: The zero subspace is a proper subset of nonzero Hilbert lattice elements. (Contributed by NM, 9-Jun-2004) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | ch0pss |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-pss | ||
2 | necom | ||
3 | ch0le | ||
4 | 3 | biantrurd | |
5 | 2 4 | bitr3id | |
6 | 1 5 | bitr4id |