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

A2: now

assume a,b are_convergent_wrt {} ; :: thesis: a = b
then consider c being set such that
A3: ( {} reduces a,c & {} reduces b,c ) by Def7;
( a = c & b = c ) by A3, Th14;
hence a = b ; :: thesis: verum

end;

now

assume a,b are_divergent_wrt {} ; :: thesis: a = b
then consider c being set such that
A4: ( {} reduces c,a & {} reduces c,b ) by Def8;
( a = c & b = c ) by A4, Th14;
hence a = b ; :: thesis: verum

end;

hence a = b by A1, A2; :: thesis: verum