let a, b be natural Ordinal; :: thesis: ( {} / b = {} & a / 1 = a )
A1: ( b <> {} implies RED (b,{}) = 1 ) by Th26;
RED ({},b) = {} by Th26;
hence {} / b = {} by A1, Def10; :: thesis: a / 1 = a
( RED (1,a) = 1 & RED (a,1) = a ) by Th24;
hence a / 1 = a by Def10; :: thesis: verum