Theorem scutcl

Description: Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024)

	Ref	Expression
Assertion	scutcl	|- ( A < ( A |s B ) e. No )

Proof

Step	Hyp	Ref	Expression
1		scutcut	|- ( A < ( ( A |s B ) e. No /\ A <
2	1	simp1d	|- ( A < ( A |s B ) e. No )