let a be natural Ordinal; :: thesis: ( RED ({},a) = {} & ( a <> {} implies RED (a,{}) = 1 ) )
thus RED ({},a) = {} by ORDINAL3:70; :: thesis: ( a <> {} implies RED (a,{}) = 1 )
assume A1: a <> {} ; :: thesis: RED (a,{}) = 1
thus RED (a,{}) = a div^ a by Th14
.= (a *^ 1) div^ a by ORDINAL2:39
.= 1 by A1, ORDINAL3:68 ; :: thesis: verum