let x, y be ExtReal; :: thesis: for a, b being Real st x = a & y = b holds

x - y = a - b

let a, b be Real; :: thesis: ( x = a & y = b implies x - y = a - b )

assume A1: x = a ; :: thesis: ( not y = b or x - y = a - b )

assume y = b ; :: thesis: x - y = a - b

then - y = - b by XXREAL_3:def 3;

hence x - y = a - b by A1, XXREAL_3:def 2; :: thesis: verum

x - y = a - b

let a, b be Real; :: thesis: ( x = a & y = b implies x - y = a - b )

assume A1: x = a ; :: thesis: ( not y = b or x - y = a - b )

assume y = b ; :: thesis: x - y = a - b

then - y = - b by XXREAL_3:def 3;

hence x - y = a - b by A1, XXREAL_3:def 2; :: thesis: verum