let F, G be ext-real-membered set ; :: thesis: F /// G = { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) }
thus F /// G c= { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } :: according to XBOOLE_0:def 10 :: thesis: { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } c= F /// G

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in F /// G or e in { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } )
assume e in F /// G ; :: thesis: e in { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) }
then consider w1, w2 being Element of ExtREAL such that
A1: e = w1 * w2 and
A2: w1 in F and
A3: w2 in G "" ;
consider w being Element of ExtREAL such that
A4: w2 = w " and
A5: w in G by A3;
e = w1 / w by A1, A4;
hence e in { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } by A2, A5; :: thesis: verum

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } or e in F /// G )
assume e in { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ; :: thesis: e in F /// G
then consider w1, w2 being Element of ExtREAL such that
A6: ( e = w1 / w2 & w1 in F ) and
A7: w2 in G ;
w2 " in G "" by A7;
hence e in F /// G by A6; :: thesis: verum