let a, b, c be ordinal number ; :: thesis: ( 0 in a & exp (a,b) in exp (a,c) implies b in c )
assume A0: ( 0 in a & exp (a,b) in exp (a,c) ) ; :: thesis: b in c
assume not b in c ; :: thesis: contradiction
then exp (a,c) c= exp (a,b) by A0, ORDINAL4:27, ORDINAL1:26;
then exp (a,b) in exp (a,b) by A0;
hence contradiction ; :: thesis: verum