for A, B, C being Ordinal st C <> {} & A in B +^ C holds
A -^ B in C