let a be natural Ordinal; :: thesis: ( RED {} ,a = {} & ( a <> {} implies RED a,{} = 1 ) )
thus RED {} ,a = {} by ORDINAL3:83; :: thesis: ( a <> {} implies RED a,{} = 1 )
assume A1: a <> {} ; :: thesis: RED a,{} = 1
thus RED a,{} = a div^ a by Th19
.= (a *^ 1) div^ a by ORDINAL2:56
.= 1 by A1, ORDINAL3:81 ; :: thesis: verum