Metamath Proof Explorer


Theorem ch0lei

Description: The closed subspace zero is the smallest member of CH . (Contributed by NM, 15-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypothesis ch0le.1
|- A e. CH
Assertion ch0lei
|- 0H C_ A

Proof

Step Hyp Ref Expression
1 ch0le.1
 |-  A e. CH
2 ch0le
 |-  ( A e. CH -> 0H C_ A )
3 1 2 ax-mp
 |-  0H C_ A