set G = G_Real ;
let a be Element of G_Real ; :: thesis: ex b being Element of G_Real st b + b = a
reconsider a = a as Element of REAL ;
reconsider b' = a / 2 as Real ;
consider b being Element of G_Real such that
A1: b = b' ;
b + b = a by A1;
hence ex b being Element of G_Real st b + b = a ; :: thesis: verum