let a be natural Ordinal; :: thesis: ( a <> {} implies a / a = 1 )
assume a <> {} ; :: thesis: a / a = 1
then RED (a,a) = 1 by Th27;
hence a / a = 1 by Def10; :: thesis: verum