Metamath Proof Explorer

Theorem ch0le

Description: The zero subspace is the smallest member of CH . (Contributed by NM, 14-Aug-2002) (New usage is discouraged.)

Ref Expression
Assertion ch0le 
|- ( A e. CH -> 0H C_ A )

Proof

Step Hyp Ref Expression
1 chsh 
 |-  ( A e. CH -> A e. SH )
2 sh0le 
 |-  ( A e. SH -> 0H C_ A )
3 1 2 syl 
 |-  ( A e. CH -> 0H C_ A )