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