Metamath Proof Explorer

Theorem shsub2

Description: Subspace sum is an upper bound of its arguments. (Contributed by NM, 17-Dec-2004) (New usage is discouraged.)

Ref Expression
Assertion shsub2 
|- ( ( A e. SH /\ B e. SH ) -> A C_ ( B +H A ) )

Proof

Step Hyp Ref Expression
1 shsub1 
 |-  ( ( A e. SH /\ B e. SH ) -> A C_ ( A +H B ) )
2 shscom 
 |-  ( ( A e. SH /\ B e. SH ) -> ( A +H B ) = ( B +H A ) )
3 1 2 sseqtrd 
 |-  ( ( A e. SH /\ B e. SH ) -> A C_ ( B +H A ) )