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