const ordinal : set prop const ordsucc : set set const Empty : set axiom ordinal_1: ordinal (ordsucc Empty) const In : set set prop term iIn = In infix iIn 2000 2000 axiom In_0_1: Empty iIn ordsucc Empty const SNoLt : set set prop term < = SNoLt infix < 2020 2020 axiom ordinal_In_SNoLt: !x:set.ordinal x -> !y:set.y iIn x -> y < x claim Empty < ordsucc Empty