Theorem press

Description: Predecessor is a subset of its successor. (Contributed by Peter Mazsa, 12-Jan-2026)

	Ref	Expression
Assertion	press	Could not format assertion : No typesetting found for |- ( N e. Suc -> pre N C_ N ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		sssucid	Could not format pre N C_ suc pre N : No typesetting found for |- pre N C_ suc pre N with typecode |-
2		sucpre	Could not format ( N e. Suc -> suc pre N = N ) : No typesetting found for |- ( N e. Suc -> suc pre N = N ) with typecode |-
3	1 2	sseqtrid	Could not format ( N e. Suc -> pre N C_ N ) : No typesetting found for |- ( N e. Suc -> pre N C_ N ) with typecode |-