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