let a, b be set ; :: 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 set such that
A2: {} reduces a,c and
A3: {} reduces b,c by Def7;
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 set such that
A5: {} reduces c,a and
A6: {} reduces c,b by Def8;
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