hereby :: thesis: ( ( not 1 in b or not 0 in a ) implies ex b₁ being Ordinal st b₁ = 0 )

assume A1: ( 1 in b & 0 in a ) ; :: thesis: ex c being Ordinal st
( exp (b,c) c= a & ( for d being Ordinal st exp (b,d) c= a holds
not d c/= c ) )
defpred S₁[ Ordinal] means a c= exp (b,$1);
a c= exp (b,a) by A1, ORDINAL4:32;
then A2: ex c being Ordinal st S₁[c] ;
consider c being Ordinal such that
A3: ( S₁[c] & ( for d being Ordinal st S₁[d] holds
c c= d ) ) from ORDINAL1:sch 1(A2);
0 in Segm 1 by NAT_1:44;
then A4: 0 in b by A1, ORDINAL1:10;

per cases ( a = exp (b,c) or a c< exp (b,c) ) by A3;

suppose A5: a = exp (b,c) ; :: thesis: ex c being Ordinal st
( exp (b,c) c= a & ( for d being Ordinal st exp (b,d) c= a holds
not d c/= c ) )

take c = c; :: thesis: ( exp (b,c) c= a & ( for d being Ordinal st exp (b,d) c= a holds
not d c/= c ) )
thus exp (b,c) c= a by A5; :: thesis: for d being Ordinal st exp (b,d) c= a holds
not d c/= c
let d be Ordinal; :: thesis: ( exp (b,d) c= a implies not d c/= c )
assume A6: ( exp (b,d) c= a & d c/= c ) ; :: thesis: contradiction
then c in d by ORDINAL1:16;
then a in exp (b,d) by A1, A5, ORDINAL4:24;
then a in a by A6;
hence contradiction ; :: thesis: verum

end;

suppose A7: a c< exp (b,c) ; :: thesis: ex d being Ordinal st
( exp (b,d) c= a & ( for e being Ordinal st exp (b,e) c= a holds
not e c/= d ) )

then A8: a in exp (b,c) by ORDINAL1:11;
succ 0 c= a by A1, ORDINAL1:21;
then ( 1 in exp (b,c) & exp (b,0) = 1 ) by A7, ORDINAL1:11, ORDINAL1:12, ORDINAL2:43;
then A9: c <> 0 ;

now :: thesis: not c is limit_ordinal

assume c is limit_ordinal ; :: thesis: contradiction
then consider d being Ordinal such that
A10: ( d in c & a in exp (b,d) ) by A9, A4, A8, Th11;
S₁[d] by A10, ORDINAL1:def 2;
then c c= d by A3;
then d in d by A10;
hence contradiction ; :: thesis: verum

end;

then consider d being Ordinal such that
A11: c = succ d by ORDINAL1:29;
take d = d; :: thesis: ( exp (b,d) c= a & ( for e being Ordinal st exp (b,e) c= a holds
not e c/= d ) )
thus exp (b,d) c= a :: thesis: for e being Ordinal st exp (b,e) c= a holds
not e c/= d

proof

assume exp (b,d) c/= a ; :: thesis: contradiction
then a c= exp (b,d) ;
then c c= d by A3;
then d in d by A11, ORDINAL1:21;
hence contradiction ; :: thesis: verum

end;

let e be Ordinal; :: thesis: ( exp (b,e) c= a implies not e c/= d )
assume A12: ( exp (b,e) c= a & e c/= d ) ; :: thesis: contradiction
then d in e by ORDINAL1:16;
then c c= e by A11, ORDINAL1:21;
then exp (b,c) c= exp (b,e) by A1, ORDINAL4:27;
then a in exp (b,e) by A8;
then a in a by A12;
hence contradiction ; :: thesis: verum

end;

end;

end;

thus ( ( not 1 in b or not 0 in a ) implies ex b₁ being Ordinal st b₁ = 0 ) ; :: thesis: verum