let F be ext-real-membered set ; :: thesis: for f being ext-real number holds F /// f = { (w / f) where w is Element of ExtREAL : w in F }
let f be ext-real number ; :: thesis: F /// f = { (w / f) where w is Element of ExtREAL : w in F }
thus F /// f c= { (w / f) where w is Element of ExtREAL : w in F } :: according to XBOOLE_0:def 10 :: thesis: { (w / f) where w is Element of ExtREAL : w in F } c= F /// f

proof

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

end;

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (w / f) where w is Element of ExtREAL : w in F } or e in F /// f )
assume e in { (w / f) where w is Element of ExtREAL : w in F } ; :: thesis: e in F /// f
then ex w being Element of ExtREAL st
( e = w / f & w in F ) ;
hence e in F /// f by Th229; :: thesis: verum