Description: The size of a subset of a finite set is less than the size of the containing set. (Contributed by Glauco Siliprandi, 11-Dec-2019) TODO (NM): usage (2 times) should be replaced by hashss , and hashssle should be deleted afterwards.
Ref | Expression | ||
---|---|---|---|
Assertion | hashssle | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hashss | |