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
A12: ( exp (b,d1) c= a & ( for c being ordinal number st exp (b,c) c= a holds
c c= d1 ) ) and
A13: ( 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 A12, A13; :: according to XBOOLE_0:def 10 :: thesis: d2 c= d1
thus d2 c= d1 by A12, A13; :: thesis: verum

end;

end;

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