reconsider A = succ {} as Ordinal by Th13;
take A ; :: thesis: not A is empty
thus not A is empty ; :: thesis: verum