let d1, d2 be Ordinal; :: thesis: ( ( 1 in b & 0 in a & exp b,d1 c= a & ( for c being ordinal number st exp b,c c= a holds
c c= d1 ) & exp b,d2 c= a & ( for c being ordinal number st exp b,c c= a holds
c c= d2 ) implies d1 = d2 ) & ( ( not 1 in b or not 0 in a ) & d1 = 0 & d2 = 0 implies d1 = d2 ) )

hereby :: thesis: ( ( not 1 in b or not 0 in a ) & d1 = 0 & d2 = 0 implies d1 = d2 )

assume that
( 1 in b & 0 in a ) and
A1: ( exp b,d1 c= a & ( for c being ordinal number st exp b,c c= a holds
c c= d1 ) ) and
A2: ( exp b,d2 c= a & ( for c being ordinal number st exp b,c c= a holds
c c= d2 ) ) ; :: thesis: d1 = d2
thus d1 = d2 :: thesis: verum

proof

thus d1 c= d2 by A1, A2; :: according to XBOOLE_0:def 10 :: thesis: d2 c= d1
thus d2 c= d1 by A1, A2; :: thesis: verum

end;

end;

thus ( ( not 1 in b or not 0 in a ) & d1 = 0 & d2 = 0 implies d1 = d2 ) ; :: thesis: verum