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