let B, A, C be Ordinal; :: thesis: ( B *^ A in C *^ A implies B in C )
assume A1: ( B *^ A in C *^ A & not B in C ) ; :: thesis: contradiction
then C c= B by ORDINAL1:26;
hence contradiction by A1, ORDINAL1:7, ORDINAL2:58; :: thesis: verum