let a1, b1 be Real; :: thesis: for a2, b2 being R_eal st a1 = a2 & b1 = b2 holds
a1 - b1 = a2 - b2
let a2, b2 be R_eal; :: thesis: ( a1 = a2 & b1 = b2 implies a1 - b1 = a2 - b2 )
assume A1: ( a1 = a2 & b1 = b2 ) ; :: thesis: a1 - b1 = a2 - b2
a2 - b2 = a2 + (- b2) by XXREAL_3:def 4;
then a2 - b2 = a2 + (- b1) by A1, XXREAL_3:def 3;
then a2 - b2 = a1 + (- b1) by A1, XXREAL_3:def 2;
hence a1 - b1 = a2 - b2 ; :: thesis: verum