for A, B, C being Ordinal st A in B *^ C & B is limit_ordinal holds
ex D being Ordinal st
( D in B & A in D *^ C )