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

assume A: ( 1 in b & 0 in a ) ; :: thesis: ex c being ordinal number st
( exp (b,c) c= a & ( for d being ordinal number 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 A, ORDINAL4:32;
then A0: ex c being ordinal number st S₁[c] ;
consider c being ordinal number such that
A1: ( S₁[c] & ( for d being ordinal number st S₁[d] holds
c c= d ) ) from ORDINAL1:sch 1(A0);
0 in 1 by NAT_1:45;
then A2: 0 in b by A, ORDINAL1:19;

per cases ( a = exp (b,c) or a c< exp (b,c) ) by A1, XBOOLE_0:def 8;

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

take c = c; :: thesis: ( exp (b,c) c= a & ( for d being ordinal number st exp (b,d) c= a holds
not d c/= c ) )
thus exp (b,c) c= a by B1; :: thesis: for d being ordinal number st exp (b,d) c= a holds
not d c/= c
let d be ordinal number ; :: thesis: ( exp (b,d) c= a implies not d c/= c )
assume B2: ( exp (b,d) c= a & d c/= c ) ; :: thesis: contradiction
then c in d by ORDINAL1:26;
then a in exp (b,d) by A, B1, ORDINAL4:24;
then a in a by B2;
hence contradiction ; :: thesis: verum

end;

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

then C1: a in exp (b,c) by ORDINAL1:21;
succ 0 c= a by A, ORDINAL1:33;
then ( 1 in exp (b,c) & exp (b,0) = 1 ) by C1, ORDINAL1:22, ORDINAL2:60;
then C4: c <> 0 ;

now

assume c is limit_ordinal ; :: thesis: contradiction
then consider d being ordinal number such that
C2: ( d in c & a in exp (b,d) ) by C4, A2, C1, Th005;
S₁[d] by C2, ORDINAL1:def 2;
then c c= d by A1;
then d in d by C2;
hence contradiction ; :: thesis: verum

end;

then consider d being ordinal number such that
C3: c = succ d by ORDINAL1:42;
take d = d; :: thesis: ( exp (b,d) c= a & ( for e being ordinal number st exp (b,e) c= a holds
not e c/= d ) )
thus exp (b,d) c= a :: thesis: for e being ordinal number 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 A1;
then d in d by C3, ORDINAL1:33;
hence contradiction ; :: thesis: verum

end;

let e be ordinal number ; :: thesis: ( exp (b,e) c= a implies not e c/= d )
assume B2: ( exp (b,e) c= a & e c/= d ) ; :: thesis: contradiction
then d in e by ORDINAL1:26;
then c c= e by C3, ORDINAL1:33;
then exp (b,c) c= exp (b,e) by A, ORDINAL4:27;
then a in exp (b,e) by C1;
then a in a by B2;
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