let a, b be object ; :: thesis: ( ( a,b are_convergent_wrt {} or a,b are_divergent_wrt {} ) implies a = b )

A1: now :: thesis: ( a,b are_convergent_wrt {} & ( a,b are_convergent_wrt {} or a,b are_divergent_wrt {} ) implies a = b )

assume a,b are_convergent_wrt {} ; :: thesis: ( ( a,b are_convergent_wrt {} or a,b are_divergent_wrt {} ) implies a = b )
then consider c being object such that
A2: {} reduces a,c and
A3: {} reduces b,c ;
a = c by A2, Th13;
hence ( ( a,b are_convergent_wrt {} or a,b are_divergent_wrt {} ) implies a = b ) by A3, Th13; :: thesis: verum

end;

A4: now :: thesis: ( a,b are_divergent_wrt {} & ( a,b are_convergent_wrt {} or a,b are_divergent_wrt {} ) implies a = b )

assume a,b are_divergent_wrt {} ; :: thesis: ( ( a,b are_convergent_wrt {} or a,b are_divergent_wrt {} ) implies a = b )
then consider c being object such that
A5: {} reduces c,a and
A6: {} reduces c,b ;
a = c by A5, Th13;
hence ( ( a,b are_convergent_wrt {} or a,b are_divergent_wrt {} ) implies a = b ) by A6, Th13; :: thesis: verum

end;

assume ( a,b are_convergent_wrt {} or a,b are_divergent_wrt {} ) ; :: thesis: a = b
hence a = b by A1, A4; :: thesis: verum