Intuitionize ordtr in iset.mm
Intuitionize ordtr in iset.mm

The proof is essentially unchanged, since df-ord and df-iord
both have Tr A as a left conjunct.

metamath/set.mm,metamath/set.mm,metamath/set.mm