let f, h, i be ext-real number ; :: thesis: {f} -- {h,i} = {(f - h),(f - i)}
thus {f} -- {h,i} = {f} ++ {(- h),(- i)} by Th16
.= {(f - h),(f - i)} by Th50 ; :: thesis: verum