for a, b being Ordinal
for x being object st 0 in a & not b is empty & b is limit_ordinal holds
( x in exp (a,b) iff ex c being Ordinal st
( c in b & x in exp (a,c) ) )