Theorem thincssc

Description: A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024)

	Ref	Expression
Assertion	thincssc	Could not format assertion : No typesetting found for |- ThinCat C_ Cat with typecode |-

Proof

Step	Hyp	Ref	Expression
1		thincc	Could not format ( c e. ThinCat -> c e. Cat ) : No typesetting found for |- ( c e. ThinCat -> c e. Cat ) with typecode |-
2	1	ssriv	Could not format ThinCat C_ Cat : No typesetting found for |- ThinCat C_ Cat with typecode |-