Proofgold Proof

pf
Assume H0: ordinal (Sing 1). Apply H0 with False. Assume H1: TransSet (Sing 1). Assume H2: ∀ x0 . x0 ∈ Sing 1 ⟶ TransSet x0. Apply not_TransSet_Sing1. The subproof is completed by applying H1. ■