Let x0 of type ι be given.
Let x1 of type ι be given.
Apply or3E with
prim1 x0 x1,
x0 = x1,
prim1 x1 x0,
or (prim1 x0 x1) (Subq x1 x0) leaving 4 subgoals.
Apply ordinal_trichotomy_or with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply orIL with
prim1 x0 x1,
Subq x1 x0.
The subproof is completed by applying H2.
Assume H2: x0 = x1.
Apply orIR with
prim1 x0 x1,
Subq x1 x0.
Apply H2 with
λ x2 x3 . Subq x1 x3.
The subproof is completed by applying Subq_ref with x1.
Apply orIR with
prim1 x0 x1,
Subq x1 x0.
Apply ordinal_TransSet with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.