Description: Subset implies subset of subspace sum. (Contributed by NM, 18-Nov-2000) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | shincl.1 | ||
shincl.2 | |||
shless.1 | |||
Assertion | shlessi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | shincl.1 | ||
2 | shincl.2 | ||
3 | shless.1 | ||
4 | shless | ||
5 | 4 | ex | |
6 | 1 2 3 5 | mp3an |