let B, A, 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:26;
hence contradiction by A1, ORDINAL1:7, ORDINAL2:58; :: thesis: verum