let A, B, C be Ordinal; :: thesis: ( B *^ A in C *^ A implies B in C )
assume that
A1: B *^ A in C *^ A and
A2: not B in C ; :: thesis: contradiction
C c= B by A2, ORDINAL1:16;
hence contradiction by A1, ORDINAL1:5, ORDINAL2:41; :: thesis: verum