let G be ext-real-membered set ; :: thesis: for g, f being ext-real number st g in G holds
f + g in f ++ G
let g, f be ext-real number ; :: thesis: ( g in G implies f + g in f ++ G )
f in {f} by TARSKI:def 1;
hence ( g in G implies f + g in f ++ G ) by Th39; :: thesis: verum