Let x0 of type ι be given.

Assume H0: ordinal x0.

Let x1 of type ι → ο be given.

Apply andI with PNo_strict_upperbd (PNoCutL x0 x1) x0 x1, PNo_strict_lowerbd (PNoCutR x0 x1) x0 x1 leaving 2 subgoals.

Let x2 of type ι be given.

Assume H1: ordinal x2.

Let x3 of type ι → ο be given.

Assume H2: PNoCutL x0 x1 x2 x3.

Apply H2 with PNoLt x2 x3 x0 x1.

Assume H3: x2 ∈ x0.

Assume H4: PNoLt x2 x3 x0 x1.

The subproof is completed by applying H4.

Let x2 of type ι be given.

Assume H1: ordinal x2.

Let x3 of type ι → ο be given.

Assume H2: PNoCutR x0 x1 x2 x3.

Apply H2 with PNoLt x0 x1 x2 x3.

Assume H3: x2 ∈ x0.

Assume H4: PNoLt x0 x1 x2 x3.

The subproof is completed by applying H4.

■

Proofgold Proof