let a, b be set ; :: thesis: ( a,b are_convertible_wrt {} implies a = b )
assume a,b are_convertible_wrt {} ; :: thesis: a = b
then ( {} \/ ({} ~ ) reduces a,b & {} = {} ~ ) by Def4;
hence a = b by Th14; :: thesis: verum