let F, G be ext-real-membered set ; :: thesis: for f, g being ExtReal st f in F & g in G holds
f - g in F -- G
let f, g be ExtReal; :: thesis: ( f in F & g in G implies f - g in F -- G )
A1: ( f in ExtREAL & g in ExtREAL ) by XXREAL_0:def 1;
F -- G = { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } by Th54;
hence ( f in F & g in G implies f - g in F -- G ) by A1; :: thesis: verum