theorem :: MEMBER_1:64

for f, g, h, i being ExtReal holds {f,g} -- {h,i} = {(f - h),(f - i),(g - h),(g - i)}