let x, y be R_eal; :: 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 & y = b ) ; :: thesis: x + y = a + b
then ex a, b being Real st
( x = a & y = b & x + y = a + b ) by Def2;
hence x + y = a + b by A1; :: thesis: verum