let a, b, c be Ordinal; :: thesis: ( 0 in a & exp (a,b) in exp (a,c) implies b in c )
assume A1: ( 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 A1, ORDINAL1:16, ORDINAL4:27;
then exp (a,b) in exp (a,b) by A1;
hence contradiction ; :: thesis: verum