let G be ext-real-membered set ; :: thesis: for f, g being ExtReal st g in G holds
f - g in f -- G
let f, g be ExtReal; :: 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 Th55; :: thesis: verum