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