This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem atssch

Description: Atoms are a subset of the Hilbert lattice. (Contributed by NM, 14-Aug-2002) (New usage is discouraged.)

		Ref	Expression
	Assertion	atssch	$⊢ HAtoms \subseteq C_{ℋ}$

Step	Hyp	Ref	Expression
1		df-at	$⊢ HAtoms = \{x \in C_{ℋ} \| 0_{ℋ} ⋖_{ℋ} x\}$
2	1	ssrab3	$⊢ HAtoms \subseteq C_{ℋ}$