for A, B, C being Ordinal st A in B holds
( A in B +^ C & A in C +^ B )