let a, b be Real; :: thesis: for x, y being ExtReal st a = x & b = y holds
a - b = x - y
let x, y be ExtReal; :: thesis: ( a = x & b = y implies a - b = x - y )
assume A1: ( a = x & b = y ) ; :: thesis: a - b = x - y
reconsider c = - y as Real by A1;
A2: c = - b by A1, XXREAL_3:def 3;
x - y = x + (- y) by XXREAL_3:def 4;
then x - y = a + c by A1, XXREAL_3:def 2;
hence a - b = x - y by A2; :: thesis: verum