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 Th101;
hence ( f in F & g in G implies f / g in F /// G ) by A1; :: thesis: verum