for A being Ordinal holds Rank (succ A) = bool (Rank A) by Lm2;